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

Deducteam

Software around Dedukti and LambdaPi

Isabelle/C

Framework for test and proofs of C programs in Isabelle

Publications

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

Seminars, working groups

  • Regular Deducteam seminar on Thursday afternoon

Projects

Bilateral French-Japanese project (Hubert Curien partnership)

Members

Permanent

PhD Students

Luc Chabassier

Xavier Denis

Houda MOUHCINE

Melanie Taprogge

PostDoc

Alidra Abdelghani

Anthony Bordg

Matteo Manighetti