Friday 14 October 2016, 10:30: Reverse engineering of arithmetic proofs: from Matita to Hol, François Thiré (Deducteam).

Abstract. This talk aims to present the work I did during my graduation internship with Gilles Dowek. The problem addressed in this internship is to translate arithmetic proofs from a proof checker Matita (based on the Calculus of Construction) to HOL (a higher-order logic proof checker). The difficulty comes from that a lot of features of Matita (universes, dependent types) do not exist in HOL. Since this translation needs to modify the logic used inside the proofs Dedukti is handy here because as a logical framework, it explicits which part of the logic is used inside proofs. A part of this talk will also be dedicated to present new Dedukti tools that I used to transforms Dedukti terms.