Point of contact
Chantal Keller, LMF, Chantal.Keller@lri.fr
Summary
Many paradigms and proof systems have been developed to mechanize
logical reasoning: interactive and automatic theorem provers, proof
checkers, programming languages with strong guaranties, model
checking… This large panel covers very diverse objective, from proving
abstract mathematical theorems to certifying software and hardware. If
this diversity allows us to formally and semi-automatically verify
complex statements, it comes with a heavy duplication of efforts:
these systems rely on very different proof languages and can barely
communicate results or libraries.
Our objective is to explore proofs as communication protocols between
systems. Efforts in this direction include in particular:
• the design of a universal proof format that relies on generic and
extensible logical frameworks, that can represent and combine proofs
from various systems
• the implementation of this format with communication tools, logical
encodings, algorithms to relate proof statements, …
• the export of universal libraries that can be used in any system.
Keywords
universality of proofs, proof exchange, proof systems
Partners
- LIX, Polytechnique, CNRS (Partout team)
- LMF, Université Paris-Saclay, CNRS, École Normale Supérieure Paris-Saclay (Mechanized Proof team)
- Samovar, Télécom SudParis, CNRS (Méthodes team)
- U2IS, ENSTA (SSH team)
- Inria Saclay–Île-de-France, Inria (Partout, Toccata and Deducteam teams)
A few references
- D. Miller. A Distributed and Trusted Web of Formal Proofs. In Distributed Computing and Internet Technology (ICDCIT), 2020.
- Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui. EKSTRAKTO: A tool to reconstruct Dedukti proofs from TSTP files. Proof eXchange for Theorem Proving (PxTP), 2019.
- B. Ekici et al. SMTCoq: A plug-in for integrating SMT solvers into Coq. In Computer Aided Verification (CAV), 2017.
- Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe. Universality of Proofs. Dagstuhl Seminar 16421, 2016.
- Logipedia website: http://logipedia.inria.fr