Section: Overall Objectives

History

The idea that systems such as Euclidean geometry or set theory should be expressed, not as independent systems, but in a logical framework appeared with the design of the first logical framework: predicate logic, in 1928. Later, several more powerful logical frameworks have been designed: $\lambda$-prolog, Isabelle, the Edinburgh logical framework, Pure type systems, and Deduction modulo theory.

The logical framework that we use is a simple $\lambda$-calculus with dependent types and rewrite rules, called the $\lambda \Pi$-calculus modulo theory, and also the Martin-Löf logical framework, and it generalizes all the mentioned frameworks. It is implemented in the system Dedukti .

The first version of Dedukti was developed in 2011 by Mathieu Boespflug [29]. From 2012 to 2015, new versions of Dedukti were developed and several theories were expressed in Dedukti , allowing to import proofs developed in Matita (with the tool Krajono ), HOL Light (with the tool Holide ), FoCaLiZe (with the tool Focalide ), iProver , and Zenon , totalizing several hundred of megabytes of proofs.

From 2015 to 2018, we focused on the translation of proofs from one Dedukti theory to another and to the exporting of proofs to other proof systems. In particular the Matita arithmetic library has been translated to a much weaker theory: constructive simple type theory, allowing to export it to Coq , Lean , PVS , HOL Light , and Isabelle/HOL . This led us to develop, in 2018, an online proof encyclopedia Logipedia , allowing to share and browse this library. We also focused on the development of new theories in Dedukti , and on an interactive theorem prover on top of Dedukti .