dedukti
Version 1.1.4 revision 0 uploaded by MathieuBoespflug.
Package meta
- Synopsis
- A type-checker for the λΠ-modulo calculus.
- Description
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 [1].
- 1
- G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.
- Author
- Mathieu Boespflug
- Bug reports
- n/a
- Category
- Theorem Provers, Compilers/Interpreters
- Copyright
- © 2009 CNRS - École Polytechnique - INRIA
- Homepage
- http://www.lix.polytechnique.fr/dedukti
- Maintainer
- Mathieu Boespflug <mboes@lix.polytechnique.fr>
- Package URL
- n/a
- Stability
- n/a