dedukti

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].


Keywords
compilers-interpreters, gpl, library, program, theorem-provers, Propose Tags , Dedukti.Runtime
License
GPL-2.0+
Install
cabal install dedukti-1.1.4