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:

1. 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
2. interoperability between proof systems, by designing, using and transforming proof certificates
3. the development of libraries and formalizations in various domains:
   • for data
   • for mathematics
   • for proof of programs

Software

Publications

Full list on HAL: https://hal.science/LMF-PM

Seminars, working groups

• Regular Deducteam seminar on Thursday afternoon

Projects

Members

Permanent

PhD Students

PostDoc