By Cyril Cohen
In this talk I present Trocq, a proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq interactive theorem prover, in the Rocq-Elpi meta-language.
This is a joint work with Enzo Crance and Assia Mahboubi.
By De Lon Adrian
By Guillaume Baudart , Emilio Jesús Gallego Arias
By Jim Portegies
By Cyril Cohen
By Josef Urban
By Peter Bühlmann
By Joël Ouaknine
By Joël Ouaknine
By Joël Ouaknine
