04-20-2018 | Giles Dowek: A Proof Library Shared by Different Proof Systems

Title #2: “A Proof Library Shared by Different Proof Systems”

Speaker #2: Gilles Dowek, Researcher, Inria & Professor, École normale de Paris-Saclay

Date: Friday, April 20, 2018

Time: 2:30pm

Location: NIA, Room 137

Abstract: Gilles will present a library of proofs in arithmetic, from the definition of  natural numbers to Fermat’s little theorem, that can be used in five different systems (HOL Light, HOL 4, Isabelle / HOL, Matita, and Coq). This library, originally developed in Matita has been translated to an implementation of the Calculus of Inductive Constructions in the logical framework Dedukti, then translated to an implementation of Simple type theory in Dedukti and then exported to the these five systems.

Short Bio: Gilles Dowek is a reseacher at Inria and a professor at the École normale de Paris-Saclay. He is interested in the formalization of  mathematics, in proof processing systems, in physics of computation, and in the safety of aerospace systems. He is the author of Computation, Proof, Machine: Mathematics Enters a New Age, Cambridge University Press (2015).