A universal proof checker
What is Dedukti ?
Dedukti is a universal proof checker, based on the λΠ-calculus modulo formalism.
The project is named after the word for "to deduce" in Esperanto.
Authors
Dedukti is a project of ARC Corias. The main developer is Mathieu Boespflug.Get Dedukti
The source code is distributed under the terms of the GNU General Public License (version 3 or later).
It is available as a Cabal package on hackage.haskell.org.
Reference manual
The reference manual of Dedukti is available here (PDF version).
Research papers
- Embedding Pure Types Systems in the
λΠ-calculus modulo, D. Cousineau and G. Dowek,
Typed Lambda calculi and Applications. Lecture Notes in Computer Science 4583, Springer. pp. 102-117. 2007. - Conversion by Evaluation [draft], M. Boespflug,
accepted for Practical Aspects of Declarative Languages 2010.


