Software around Dedukti and LambdaPi
Preuve mécanisée
Keywords
- automatic theorem proving
- interactive theorem proving
- interoperability of proof systems
- logical frameworks
- crossed verification
- Dedukti
- LambdaPi
Overview
This team gathers designers of mechanized proof tools, from systems to libraries, in a continuum. It has three axes:
- the design and development of proof systems, in particular:
- the design of the λΠ-calcul modulo theories formalism, put in practice through the proof checker Dedukti and the proof assistant LambdaPi
- the participation in the development of the Isabelle interactive theorem prover
- the participation in the development of Method B and Event-B
- interoperability between proof systems, by designing, using and transforming proof certificates
- the development of libraries and formalizations in various domains:
- for data
- for mathematics
- for proof of programs
Software
Formalizing data in Coq
Libraries for proofs of programs
Framework for test and proofs of C programs in Isabelle
Universal library of proofs
Software for proof automation in Coq
Publications
Full list on HAL: https://hal.science/LMF-PM
Seminars, working groups
- Regular Deducteam seminar on Thursday afternoon
Projects
Interoperable and Confident Set-based Proof Assistants
European Research Network on Formal Proofs
Members
Permanent
PhD Students
Luc Chabassier
Xavier Denis
Houda MOUHCINE
Melanie Taprogge
PostDoc
Alidra Abdelghani
Anthony Bordg
Matteo Manighetti