package lambdapi

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

Install

dune-project
 Dependency

Authors

Maintainers

Sources

lambdapi-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

Description

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.

Published: 21 Jul 2025

Dependencies (22)

  1. uri >= "1.1"
  2. lwt_ppx >= "1"
  3. stdlib-shims >= "0.1"
  4. cmdliner >= "1.1"
  5. yojson >= "1.6"
  6. why3 >= "1.8"
  7. camlp-streams >= "5"
  8. pratter >= "5" & < "6"
  9. timed >= "1"
  10. sedlex >= "3.2"
  11. menhir >= "20200624"
  12. dream = "1.0.0~alpha6"
  13. dream-httpaf = "1.0.0~alpha3"
  14. dream-pure = "1.0.0~alpha2"
  15. ocaml >= "4.10" & < "4.13"
  16. dream >= "1.0.0~alpha3"
  17. ocaml >= "4.13" & < "5.3"
  18. dream = "1.0.0~alpha8"
  19. dream-httpaf = "1.0.0~alpha4"
  20. dream-pure = "1.0.0~alpha2"
  21. ocaml >= "5.3"
  22. dune >= "3.7"

Dev Dependencies (4)

  1. odoc with-doc
  2. dedukti with-test & >= "2.7"
  3. alt-ergo with-test
  4. alcotest with-test

Used by

None

OCaml

Innovation. Community. Security.