lambdapiversion

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.

AuthorDeducteam
LicenseCECILL-2.1
Published
Homepagehttps://github.com/Deducteam/lambdapi
Issue Trackerhttps://github.com/Deducteam/lambdapi/issues
Maintainerdedukti-dev@inria.fr
Dependencies
Conflicts
Source [http] https://github.com/Deducteam/lambdapi/releases/download/2.5.1/lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/lambdapi/lambdapi.2.5.1/opam
No package is dependent