Home

Dedukti 1.0 is out !

Fri, 2009-10-09 22:47 | by notin

The TypiCal team is pleased to announce the first release of Dedukti. Dedukti is a proof checker for the λΠ-calculus modulo. It aims at verifying proofs generated by various proof assistants by translating proofs into a universal framework mixing λΠ-calculus and rewrite rules.