LaTTe : a laboratory of type theory experiments

Team : APR

LaTTe is a proof assistant library based on type theory. The specific feature of LaTTe is its design as a library (unlike most proof assistant, generally designed as standalone tools) tightly integrated with the Clojure language and ecosystem. This enables "proving in the large": sharing mathematical contents across the internet in a collaborative way. It also provides a domain specific language for declarative proofs, based on "fitch-style" proofs for natural deduction. The tool is developed by members of the APR team in a collaboration with the Whisper team (Pierre-Evariste Dagand).

Software leader : Frédéric PESCHANSKI