Lambdapi User Manual¶
Lambdapi is a proof assistant for the λΠ-calculus modulo rewriting. See What is Lambdapi? for more details.
Lambdapi files must end with .lp
. But Lambdapi can also read
Dedukti files ending with .dk
and convert them to Lambdapi files (see Compatibility with Dedukti).
Installation instructions - Frequently Asked Questions - Issue tracker
Examples of developments made with Lambdapi:
Opam repository of Lambdapi libraries