Release of Lambdapi 2.1.0

[Frédéric Blanqui]

Dear all,

I am pleased to announce the release 2.1.0 of Lambdapi on opam.

See https://github.com/Deducteam/lambdapi for more details
and https://lambdapi.readthedocs.io/ for its user manual.

Lambdapi is a proof assistant for the λΠ-calculus modulo rewriting.

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). The declaration
of symbols and rewriting rules is separated so that one can
easily define inductive-recursive types for instance.
Rewrite rules can be exported to the TRS and XTC formats
for checking confluence and termination with external tools.
A symbol can be declared associative and commutative.
Lambdapi supports unicode symbols and infix operators.

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.

Lambdapi is mostly compatible with Dedukti: it can read .dk files
and convert .lp files to .dk files. Dedukti is just a type checker
and has no features such as implicit arguments, etc. Hence,
Lambdapi can be used as a higher-level intermediate language
to translate proofs from a given proof system to Dedukti.

Best regards,

Frédéric.