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).