Lambdapi is an interactive proof assistant based on the λΠ-calculus modulo rewriting.
It combines dependent types with user-defined rewriting rules, letting you define objects and types using oriented equations and reason modulo those equations.
The software is also a logical framework and does not impose a predefined logic. It can read and write Dedukti files and offers some support for exporting definitions and proofs to Coq.
This is free and open source software.
Key Features
- Supports dependent types and user-defined rewriting rules.
- Interactive resolution of typing and unification goals using tactics.
- Supports Unicode and user-defined infix operators.
- Symbols can be declared commutative, or associative and commutative.
- Supports implicit arguments whose values are inferred automatically.
- Provides a rewrite tactic similar to SSReflect in Coq.
- Can call external automated provers.
- Generates induction principles for strictly positive inductive types.
- Can check confluence and termination of user-defined rewriting rules using external provers.
- Offers Emacs and Visual Studio Code plugins based on LSP.
- Provides compatibility with Dedukti files.
Website: github.com/deducteam/lambdapi
Support:
Developer: Deducteam
License: CECILL-2.1
Lambdapi is written in OCaml. Learn OCaml with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |