What is Lambdapi?

Lambdapi is an interactive proof system featuring dependent types like in Martin-Lőf’s type theory, but allowing to define objects and types using oriented equations, aka rewriting rules, and reason modulo those equations.

This allows to simplify some proofs, and formalize complex mathematical objects that are otherwise impossible or difficult to formalize in more traditional proof systems.

Lambdapi can also take as input Dedukti files, and can thus be used as an interoperability tool.

Lambdapi is a logical framework and does not come with a pre-defined logic. However, it is easy to define a logic by a few symbols and rules. See for instance, the file FOL.lp which defines (polymorphic) first-order logic. There also exist definitions for the logics of HOL, Coq or Agda.

Here are some of the features of Lambdapi:

  • Emacs and VSCode plugins (based on LSP)
  • support for unicode (UTF-8) and user-defined infix operators
  • symbols can be declared commutative, or associative and commutative
  • some arguments can be declared as implicit: the system will try to find out their value automatically
  • symbol and rule declarations are separated so that one can easily define inductive-recursive types or turn a proved equation into a rewriting rule
  • support for interactive resolution of typing goals, and unification goals as well, using tactics
  • a rewrite tactic similar to the one of SSReflect in Coq
  • the possibility of calling external automated provers
  • a command is provided for automatically generating an induction principle for (mutually defined) strictly-positive inductive types
  • Lambdapi can call external provers for checking the confluence and termination of user-defined rewriting rules by translating them to the XTC and HRS formats used in the termination and confluence competitions

Some bibliographic references