lambdapiversion Documentation on ocaml.org
Proof assistant for the λΠ-calculus modulo rewriting
Lambdapi is an interactive proof assistant for the λΠ-calculus modulo rewriting. It can call external automated theorem provers via Why3. The user manual is on https://lambdapi.readthedocs.io/. A standard library and other developments are available on https://github.com/Deducteam/opam-lambdapi-repository/. An extension for Emacs is available on MELPA. An extension for VSCode is available on the VSCode Marketplace. Lambdapi can read Dedukti files. It includes checkers for local confluence and subject reduction. It also provides commands to export Lambdapi files to other formats or systems: Dedukti, Coq, HRS, CPF.
| Author | Deducteam and friends |
|---|---|
| License | CECILL-2.1 |
| Published | |
| Homepage | https://github.com/Deducteam/lambdapi |
| Issue Tracker | https://github.com/Deducteam/lambdapi/issues |
| Maintainer | dedukti-dev@inria.fr |
| Dependencies |
|
| Source [http] | https://github.com/Deducteam/lambdapi/releases/download/4.0.0/lambdapi-4.0.0.tbz sha256=0e2e73e0ea0c674f1263bf85ed3453ed3d6084d38eea29974a03ba9e382d29d7 sha512=2831db57fcd09206687a92fc9ee7d363e87bcec5167949e9c8161d41c63d5887b9f3556bfd63a7a9a0c12e5a5dc61a397baf4f496ebdb2a2fce122142c05e7a1 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/lambdapi/lambdapi.4.0.0/opam |
No package is dependent
