Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Cauderlier, Raphaël; Dubois, Catherine: Objects and subtyping in the $\lambda$-$\Pi$-calculus modulo (2015)
- Miller, Dale: Proof checking and logic programming (2015)
- Cousineau, Denis: On completeness of reducibility candidates as a semantics of strong normalization (2012)