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

Learn Lambdapi in 15 minutes

Examples of developments made with Lambdapi:

• Some logic definitions

• Library on natural numbers, integers and polymorphic lists

• Example of inductive-recursive type definition

• Example of inductive-inductive type definition

• Test files

Opam repository of Lambdapi libraries