Monday 9 January 2023, 10:00, room 3U47 and recorded (due to technical problems it starts around 8:10): Translating proofs from an impredicative type system to a predicative one, Thiago Felicissimo (Deducteam), joint work with Frédéric Blanqui and Ashish Kumar Barnawal.

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. We present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.