package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

github.com Readme Changelog CECILL-2.1 License Edit opam file Versions (10)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.1.0.tbz
sha256=04fac3b56d1855795d7d2d2442bc650183bcd71f676c3ea77f37240e33769ce9
sha512=37f7bec3bc48632379ca9fb3eb562a0c0387e54afbdd10fb842b8da70c6dad529bb98c14b9d7cddf44a1d5aa61bba86338d310e6a7b420e95b2996b4fbafc95c

Description

This package provides:

  • A lambdapi command for checking .lp or .dk files, translating .dk files to .lp files and vice versa, or launching an LSP server for editing .lp files.
  • A library of logic definitions and basic definitions and proofs on natural numbers and polymorphic lists.
  • A rich Emacs mode based on LSP (available on MELPA too).
  • A basic mode for Vim.
  • OCaml libraries. A VSCode extension is available on the VSCode Marketplace.

Find Lambdapi user manual on https://lambdapi.readthedocs.io/.

Lambdapi provides a rich type system with dependent types. In Lambdapi, one can define both type and function symbols by using rewriting rules (oriented equations). The declaration of symbols and rewriting rules is separated so that one can easily define inductive-recursive types for instance. Rewrite rules can be exported to the TRS and XTC formats for checking confluence and termination with external tools. A symbol can be declared associative and commutative. Lambdapi supports unicode symbols and infix operators.

Lambdapi does not come with a pre-defined logic. It is a powerful logical framework in which one can easily define its own logic and build and check proofs in this logic. There exist .lp files defining first or higher-order logic and complex type systems like in Coq or Agda.

Lambdapi provides a basic module and package system, interactive modes for proving both unification goals and typing goals, and tactics for solving them step by step. In particular, a rewrite tactic like in SSReflect, and a why3 tactic for calling external automated provers through the Why3 platform.

Published: 13 Jan 2022

README

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

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

Issues can be reported on the following issue tracker.

Questions can be asked on the following forum.

Examples of developments made with Lambdapi:

Operating systems

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

Installation via Opam

Lambdapi is under active development. A new version of the lambdapi Opam package will be released soon. For now, we advise to pin the development repository to get the latest development version:

opam pin add lambdapi https://github.com/Deducteam/lambdapi.git
opam install lambdapi # install emacs and vim support as well

The VSCode extension is available on the Marketplace.

The installation gives you:

  • a main executable lambdapi in your PATH

  • OCaml libraries

  • a lambdapi mode for vim

  • a lambdapi mode for emacs

To browse the source code documentation, you can do:

opam install odig
odig doc lambdapi

Compilation from the sources

You can get the sources using git as follows:

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

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

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

opam install dune bindlib timed sedlex menhir pratter yojson cmdliner why3 alcotest alt-ergo odoc
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:

make                        # Build lambdapi
make doc                    # Build the user documentation (avalaible on readthedocs)
make odoc                   # Build the developer documentation
make install                # Install lambdapi
make install_emacs          # Install emacs mode
make install_vscode         # Install vscode extension
make install_vim            # Install vim support

Note: 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:

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.

Dependencies (11)

  1. stdlib-shims >= "0.1.0"
  2. cmdliner >= "1.0.3" & <= "1.0.4"
  3. yojson >= "1.6.0"
  4. why3 >= "1.4" & < "1.5~"
  5. pratter >= "1.2" & < "2.0.0"
  6. timed >= "1.0"
  7. bindlib = "5.0.1"
  8. sedlex >= "2.2"
  9. menhir >= "20200624"
  10. ocaml >= "4.08.0"
  11. dune >= "2.7"

Dev Dependencies (3)

  1. odoc with-doc
  2. alt-ergo with-test
  3. alcotest with-test

Used by

None

Conflicts

None