package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
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 also 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). A symbol can be declared associative and commutative. Lambdapi supports unicode symbols and infix operators. The declaration of symbols and rewriting rules is separated so that one can easily define inductive-recursive types.
Lambdapi checks that rules are locally confluent (by checking the joinability of critical pairs) and preserve typing. Rewrite rules can also be exported to the TRS and XTC formats for checking confluence and termination with external tools.
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: 27 Feb 2024
README
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
Libraries
Lambdapi libraries can be found on the Opam repository of Lambdapi libraries.
Examples
tutorial (learn Lambdapi in 15 minutes)
Some users
Stephan Merz and Alessio Coltellacci: certification of TLAPS proofs
Claude Stolze: certification of Atelier B proofs
Jean-Paul Bodeveix: certification of Rodin proofs for Event-B
Simon Guilloud: certification of LISA proofs
Thomas Traversié: An Implementation of Set Theory with Pointed Graphs
Quentin Garchery: certification of Why3 proof task transformations
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
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:
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:
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:
eval `opam env`
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 for Why3 to know the available provers for the why3 tactic.
Using Opam, a suitable OCaml environment can be setup as follows:
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:
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:
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 (14)
Used by
None
Conflicts
None