| Title: |
Trocq:Proof Transfer for Free, Beyond Equivalence and Univalence |
| Authors: |
Cohen, Cyril; Crance, Enzo; Mahboubi, Assia |
| Source: |
Cohen, C, Crance, E & Mahboubi, A 2025, 'Trocq : Proof Transfer for Free, Beyond Equivalence and Univalence', ACM Transactions on Programming Languages and Systems, vol. 47, no. 3, pp. 1-40. https://doi.org/10.1145/3737283 |
| Publication Year: |
2025 |
| Subject Terms: |
Parametricity; Proof assistants; Proof transfer; Representation independence; Univalence |
| Description: |
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 Rocq/Coq interactive theorem prover, in the Coq-Elpi meta-language. |
| Document Type: |
article in journal/newspaper |
| Language: |
English |
| ISSN: |
0164-0925; 1558-4593 |
| Relation: |
info:eu-repo/semantics/altIdentifier/hdl/https://hdl.handle.net/1871.1/7c2b9718-5b5e-46cb-bc0e-d193cced4917; info:eu-repo/semantics/altIdentifier/pissn/0164-0925; info:eu-repo/semantics/altIdentifier/eissn/1558-4593 |
| DOI: |
10.1145/3737283 |
| Availability: |
https://research.vu.nl/en/publications/7c2b9718-5b5e-46cb-bc0e-d193cced4917; https://doi.org/10.1145/3737283; https://hdl.handle.net/1871.1/7c2b9718-5b5e-46cb-bc0e-d193cced4917; https://www.scopus.com/pages/publications/105028494346; https://www.scopus.com/pages/publications/105028494346#tab=citedBy |
| Rights: |
info:eu-repo/semantics/openAccess ; http://creativecommons.org/licenses/by/4.0/ |
| Accession Number: |
edsbas.39891DF7 |
| Database: |
BASE |