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 <ani:sans-serif>Rocq/Coq</ani:sans-serif> interactive theorem prover, in the <ani:sans-serif>Coq-Elpi</ani:sans-serif> meta-language.
| Original language | English |
|---|---|
| Pages (from-to) | 1-40 |
| Number of pages | 40 |
| Journal | ACM Transactions on Programming Languages and Systems |
| Volume | 47 |
| Issue number | 3 |
| Early online date | 15 Sept 2025 |
| DOIs | |
| Publication status | Published - 2025 |
Bibliographical note
Publisher Copyright:© 2025 Copyright held by the owner/author(s).
Keywords
- Parametricity
- Proof assistants
- Proof transfer
- Representation independence
- Univalence
Fingerprint
Dive into the research topics of 'Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver