Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi
Abstract
Abstract This article presents Trocq , a new 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 interactive theorem prover, in the meta-language.
Topics & Concepts
Computer scienceProof assistantAxiomType theoryEquivalence (formal languages)Plug-inProgramming languageProof theoryAutomated theorem provingTemplateTheoretical computer scienceType (biology)Algebra over a fieldCalculus (dental)Discrete mathematicsMathematicsMathematical proofPure mathematicsMedicineEcologyBiologyGeometryDentistryLogic, programming, and type systemsFormal Methods in VerificationParallel Computing and Optimization Techniques