···
synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
4
-
This package provides:
5
-
- A lambdapi command for checking .lp or .dk files,
6
-
translating .dk files to .lp files and vice versa,
7
-
or launching an LSP server for editing .lp files.
8
-
- A library of logic definitions and basic definitions and proofs
9
-
on natural numbers and polymorphic lists.
10
-
- A rich Emacs mode based on LSP (available on MELPA too).
11
-
- A basic mode for Vim.
13
-
A VSCode extension is also available on the VSCode Marketplace.
15
-
Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
17
-
Lambdapi provides a rich type system with dependent types.
18
-
In Lambdapi, one can define both type and function symbols
19
-
by using rewriting rules (oriented equations).
20
-
A symbol can be declared associative and commutative.
21
-
Lambdapi supports unicode symbols and infix operators.
22
-
The declaration of symbols and rewriting rules is separated
23
-
so that one can easily define inductive-recursive types.
25
-
Lambdapi checks that rules are locally confluent (by checking
26
-
the joinability of critical pairs) and preserve typing.
27
-
Rewrite rules can also be exported to the TRS and XTC formats
28
-
for checking confluence and termination with external tools.
30
-
Lambdapi does not come with a pre-defined logic. It is a
31
-
powerful logical framework in which one can easily define
32
-
its own logic and build and check proofs in this logic.
33
-
There exist .lp files defining first or higher-order logic
34
-
and complex type systems like in Coq or Agda.
36
-
Lambdapi provides a basic module and package system,
37
-
interactive modes for proving both unification goals
38
-
and typing goals, and tactics for solving them step by step.
39
-
In particular, a rewrite tactic like in SSReflect, and
40
-
a why3 tactic for calling external automated provers through
41
-
the Why3 platform."""
4
+
Lambdapi is an interactive proof assistant for the λΠ-calculus modulo
5
+
rewriting. It can call external automated theorem provers via Why3.
6
+
The user manual is on https://lambdapi.readthedocs.io/.
7
+
A standard library and other developments are available on
8
+
https://github.com/Deducteam/opam-lambdapi-repository/. An extension
9
+
for Emacs is available on MELPA. An extension for VSCode is available
10
+
on the VSCode Marketplace. Lambdapi can read Dedukti files. It
11
+
includes checkers for local confluence and subject reduction. It also
12
+
provides commands to export Lambdapi files to other formats or
13
+
systems: Dedukti, Coq, HRS, CPF.
maintainer: ["dedukti-dev@inria.fr"]
anil.recoil.org