Lambdapi, a proof assistant based on the λΠ-calculus modulo rewriting

`>>>>>` User Manual `<<<<<`

Issues can be reported on the
issue tracker.

Questions can be asked on the
forum.

User interfaces

Emacs
VSCode

Libraries

Lambdapi libraries can be found on the Opam repository of Lambdapi libraries.

Examples

tutorial (learn Lambdapi in 15 minutes)
some logic definitions
inductive-recursive type definition
inductive-inductive type definition
library on natural numbers, integers and polymorphic lists

Some users

Melanie Taprogge: extension of the LEO-III automated theorem prover for higher-order logic producing Lambdapi proofs [github] [2024 MSc thesis]
Frédéric Blanqui: translation of HOL-Light proofs to Coq [github] [LPAR'24]
Alessio Coltellacci and Stephan Merz: extension of the Alethe proof verifier Carcara for SMT solvers producing Lambdapi proofs [github] [SMT'24] [FroCoS'25]
Geoff Sutcliffe: translator from TSTP to Lambdapi [github] [FLAIRS'25]
Guillaume Burel and Frédéric Blanqui: ZenonModulo automated theorem prover for first-order logic producing Lambdapi proofs [github]
Anne Grieu and Jean-Paul Bodeveix: certification of Event-B proofs generated by Rodin in Lambdapi [ABZ'24] [ABZ'25]
Alessio Coltellacci and Stephan Merz: encoding of TLA+ set theory in Lambdapi [ABZ'23]
Nicolas Margulies: formalization of cubical type theory in Lambdapi [github]
Amélie Ledein and Elliot Butte: translation of MetaMath to Lambdapi [github] [JFLA'23]
Amélie Ledein: translation of K to Lambdapi [github] [JFLA'22] [TYPES'22]
Thomas Traversié: implementation of set theory with pointed graphs [LFMTP'22]
Luc Chabassier: formalization of some category theory [github] and of extensional type theory [github] [2025 PhD thesis]
Gabriel Hondet: translation of PVS statements to Lambdapi [github] [2022 PhD thesis]
Quentin Garchery: certification of Why3 proof task transformations in Lambdapi [PxTP'21] [2022 PhD thesis]

Operating systems

Lambdapi requires a Unix-like system. It might be possible to make it work on Windows too with Cygwin or "bash on Windows".

Installation via Opam

bash
opam install lambdapi

gives you the command lambdapi.

The Emacs extension is available on MELPA.

The VSCode extension is available on the Marketplace.

To browse the source code documentation, you can do:

bash
opam install odig
odig doc lambdapi

To install Lambdapi libraries, see the opam-lambdapi-repository.

Remark: To install Opam, see here.

To make sure that programs installed via opam are in your path, you
should have in your .bashrc (or any other shell initial file) the
following line that can be automatically added when you do opam init:

bash
test -r ~/.opam/opam-init/init.sh && . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

To update your path, you can also do:

bash
eval `opam env`

Compilation from the sources

You can get the sources using git as follows:

bash
git clone https://github.com/Deducteam/lambdapi.git

Dependencies are described in lambdapi.opam. The command why3 config detect must be run for Why3 to know the available provers for
the why3 tactic.

Using Opam, a suitable OCaml environment can be setup as follows:

bash
cd lambdapi
opam install .
why3 config detect

To compile Lambdapi, just run the command make in the source directory.
This produces the _build/install/default/bin/lambdapi binary.
Use the --help option for more information. Other make targets are:

bash
make                        # Build lambdapi
make doc                    # Build the user documentation (avalaible on readthedocs)
make bnf                    # Build the BNF grammar
make odoc                   # Build the developer documentation
make install                # Install lambdapi
make install_emacs_mode     # Install emacs mode
make install_vim_mode       # Install vim mode

You can run lambdapi without installing it with dune exec -- lambdapi.

For running tests, one also needs
alcotest and
alt-ergo.

For building the source code documentation, one needs
odoc. The starting file of the source
code html documentation is
_build/default/_doc/_html/lambdapi/index.html.

For building the User Manual, see doc/README.md.

The following commands can be used to clean up the repository:

bash
make clean     # Removes files generated by OCaml.
make distclean # Same as clean, but also removes library checking files.
make fullclean # Same as distclean, but also removes downloaded libraries.