Thursday 10 October 2019, 15:00, LSV library: Interoperability between CTS, François Thiré (PhD student, deducteam, LSV).

Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement the same logic. The logic of many proof systems such as Agda, Coq, Lean, Matita or the HOL family can be seen as an extension of some Cumulative Type System (CTS), a family of type systems parameterized by a specification. Hence, knowing whether a proof from one of these systems can be embedded to another require first to understand how a proof in a CTS specification can be embedded into another CTS specification. In this work, we give a new definition for the embedding of judgments between CTS specifications. This new definition has been implemented in Dedukti and used to show that effectively, the proof of Fermat's little theorem written in Matita could be translated into the HOL family systems. Our tool has been used also for other systems such as Coq. Recently, we were able to apply our tool on a geometry library developed in Coq, GeoCoq, and shown that a large part of this library could be also translated into the HOL family systems. Another interest behind this new definition of judgments embedding for CTS is that it also gives rise to a new definition for equivalence between CTS specifications which preserves the termination. In particular, we will prove some nontrivial equivalences between CTS. We think that these results could be used to prove the decidability of type checking for a very large class of CTS.