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.