package lambdapi

Overview
No Docs

You can search for identifiers within the package.

in-package search v0.2.0

Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

D

Deducteam

Maintainers

D

dedukti-dev@inria.fr

Sources

lambdapi-2.6.0.tbz

sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed

sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

Description

Lambdapi is an interactive proof assistant for the λΠ-calculus modulo rewriting. It can call external automated theorem provers via Why3. The user manual is on https://lambdapi.readthedocs.io/. A standard library and other developments are available on https://github.com/Deducteam/opam-lambdapi-repository/. An extension for Emacs is available on MELPA. An extension for VSCode is available on the VSCode Marketplace. Lambdapi can read Dedukti files. It includes checkers for local confluence and subject reduction. It also provides commands to export Lambdapi files to other formats or systems: Dedukti, Coq, HRS, CPF.

Published: 04 Feb 2025

Dependencies (14)

dream >= "1.0.0~alpha3"
lwt_ppx >= "1.0.0"
stdlib-shims >= "0.1.0"
cmdliner >= "1.1.0"
yojson >= "1.6.0"
why3 >= "1.8.0"
camlp-streams >= "5.0"
pratter >= "3.0.0" & < "4"
timed >= "1.0"
bindlib >= "6.0.0"
sedlex >= "3.2"
menhir >= "20200624"
ocaml >= "4.09.0"
dune >= "3.7"

Dev Dependencies (3)

odoc with-doc
dedukti with-test & >= "2.7"
alcotest with-test

Used by

None

Conflicts (1)

ocaml-option-bytecode-only

On This Page

Description
Dependencies (14)
Dev Dependencies (3)
Used by
Conflicts (1)