Thursday 4 May 2017, 14:00: A Transfer Tactic for Dedukti and its Application to Interoperability, Raphaël Cauderlier (IRIF).

Several proof systems are able to export their proofs in Dedukti allowing independent rechecking of formal libraries. These independently translated libraries define isomorphic mathematical structures. In order to merge formal developments, coming from different proof systems, I use theorem transfer in Dedukti.
I will present a transfer tactic for Dedukti, a library of transfer theorems built using this tactic. I will also illustrate the interoperability application of this library on a correctness proof of the Sieve of Eratosthenes.