Skip to Main content Skip to Navigation

Interoperability between proof systems using the logical framework Dedukti

François Thiré 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification
Abstract : Proof systems are tools used to formally prove theorems, and in particular that software is bug-free. Proof systems provide the highest degree of confidence to prove the absence of bugs in software. However, using such tools require a high level of expertise which makes them difficult to use. The interaction with a proof system requires the user to prove and formalize many mathematical concepts. Such work is time-consuming and may require a significant amount of manpower (e.g. four-color theorem or the Hales-Kepler theorem). The diversity of proof systems has the negative consequence that these theorems (e.g. The little Fermat’s theorem) are formalized many times. This thesis investigates, both on the theoretical and the practical side, ways to translate (semi-)automatically theorems proved in one proof system to another.
Document type :
Complete list of metadata
Contributor : François Thiré <>
Submitted on : Tuesday, May 11, 2021 - 4:01:24 PM
Last modification on : Friday, May 14, 2021 - 3:30:25 AM


thesis (1).pdf
Files produced by the author(s)


  • HAL Id : tel-03224039, version 1


François Thiré. Interoperability between proof systems using the logical framework Dedukti. Computer Science [cs]. ENS Paris-Saclay, 2020. English. ⟨tel-03224039⟩



Record views


Files downloads