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.