Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Source code at GitHub https://github.com/Deducteam/lambdapi
Deducteam/lambdapi.json
{
  "createdAt": "2017-09-10T20:32:16Z",
  "defaultBranch": "master",
  "description": "Proof assistant based on the λΠ-calculus modulo rewriting",
  "fullName": "Deducteam/lambdapi",
  "homepage": "",
  "language": "OCaml",
  "name": "lambdapi",
  "pushedAt": "2025-11-25T09:16:11Z",
  "stargazersCount": 355,
  "topics": [
    "dependent-types",
    "logical-framework",
    "proof-assistant",
    "proof-checker",
    "proof-translator",
    "rewriting"
  ],
  "updatedAt": "2025-11-22T20:36:42Z",
  "url": "https://github.com/Deducteam/lambdapi"
}

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

Section titled “Lambdapi, a proof assistant based on the λΠ-calculus modulo rewriting ”

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

Section titled “>>>>> User Manual <<<<<”

Issues can be reported on the issue tracker.

Questions can be asked on the forum.

User interfaces

Section titled “User interfaces”

Libraries

Section titled “Libraries”

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

Examples

Section titled “Examples”

Some users

Section titled “Some users”

Operating systems

Section titled “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

Section titled “Installation via Opam”
Terminal window
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:

Terminal window
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:

Terminal window
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:

Terminal window
eval `opam env`

Compilation from the sources

Section titled “Compilation from the sources”

You can get the sources using git as follows:

Terminal window
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:

Terminal window
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:

Terminal window
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:

Terminal window
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.