lambdapiversion

Proof assistant for the λΠ-calculus modulo rewriting

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.

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