Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadata

https://hal.archives-ouvertes.fr/tel-03224039
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

File

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

Identifiers

  • HAL Id : tel-03224039, version 1

Citation

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

Share

Metrics

Record views

76

Files downloads

31