<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>
</p>
<div class="moz-text-flowed" style="font-family: -moz-fixed;
font-size: 12px;" lang="x-unicode">Dear all,
<br>
<br>
I am pleased to announce the release 2.1.0 of Lambdapi on opam.
<br>
<br>
See <a class="moz-txt-link-freetext" href="https://urldefense.com/v3/__https://github.com/Deducteam/lambdapi__;!!IBzWLUs!C_FSrZaalBb1YXVLqfNi3ykjifj5e9dlYpv4MKNHsgK0XFAiZtm7RR6PaftOcQ-QUG_2KjOhiRVp8A$">https://github.com/Deducteam/lambdapi</a>
for more details
<br>
and <a class="moz-txt-link-freetext" href="https://urldefense.com/v3/__https://lambdapi.readthedocs.io/__;!!IBzWLUs!C_FSrZaalBb1YXVLqfNi3ykjifj5e9dlYpv4MKNHsgK0XFAiZtm7RR6PaftOcQ-QUG_2KjPxUYuk5Q$">https://lambdapi.readthedocs.io/</a>
for its user manual.
<br>
<br>
Lambdapi is a proof assistant for the λΠ-calculus modulo
rewriting.
<br>
<br>
Lambdapi provides a rich type system with dependent types.
<br>
In Lambdapi, one can define both type and function symbols
<br>
by using rewriting rules (oriented equations). The declaration
<br>
of symbols and rewriting rules is separated so that one can
<br>
easily define inductive-recursive types for instance.
<br>
Rewrite rules can be exported to the TRS and XTC formats
<br>
for checking confluence and termination with external tools.
<br>
A symbol can be declared associative and commutative.
<br>
Lambdapi supports unicode symbols and infix operators.
<br>
<br>
Lambdapi does not come with a pre-defined logic. It is a
<br>
powerful logical framework in which one can easily define
<br>
its own logic and build and check proofs in this logic.
<br>
There exist .lp files defining first or higher-order logic
<br>
and complex type systems like in Coq or Agda.
<br>
<br>
Lambdapi provides a basic module and package system,
<br>
interactive modes for proving both unification goals
<br>
and typing goals, and tactics for solving them step by step.
<br>
In particular, a rewrite tactic like in SSReflect, and
<br>
a why3 tactic for calling external automated provers through
<br>
the Why3 platform.
<br>
<br>
Lambdapi is mostly compatible with Dedukti: it can read .dk files
<br>
and convert .lp files to .dk files. Dedukti is just a type checker
<br>
and has no features such as implicit arguments, etc. Hence,
<br>
Lambdapi can be used as a higher-level intermediate language
<br>
to translate proofs from a given proof system to Dedukti.
<br>
<br>
Best regards,
<br>
<br>
Frédéric.
<br>
<br>
<br>
</div>
</body>
</html>