{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:55:54Z","timestamp":1758056154192,"version":"3.44.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"name":"European Research Council","award":["101001995"],"award-info":[{"award-number":["101001995"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            This article presents\n            <jats:sc>Trocq<\/jats:sc>\n            , a new proof transfer framework for dependent type theory.\n            <jats:sc>Trocq<\/jats:sc>\n            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\n            <jats:sans-serif>Rocq\/Coq<\/jats:sans-serif>\n            interactive theorem prover, in the\n            <jats:sans-serif>Coq-Elpi<\/jats:sans-serif>\n            meta-language.\n          <\/jats:p>","DOI":"10.1145\/3737283","type":"journal-article","created":{"date-parts":[[2025,5,26]],"date-time":"2025-05-26T21:19:12Z","timestamp":1748294352000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3540-1050","authenticated-orcid":false,"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[{"name":"Inria, CNRS, ENS de Lyon, Universit\u00e9 Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0498-0910","authenticated-orcid":false,"given":"Enzo","family":"Crance","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, Nantes, France and Mitsubishi Electric R&amp;D Centre Europe BV Rennes, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0312-5461","authenticated-orcid":false,"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, \u00c9cole Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, Nantes, France and VU Amsterdam, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","unstructured":"Reynald Affeldt and Cyril Cohen. 2023. Measure construction by extension in dependent type theory with application to integration. arXiv:2209.02345. Retrieved from https:\/\/arxiv.org\/abs\/2209.02345","DOI":"10.1007\/s10817-023-09671-5"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575678"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632920"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. 2015. Towards a cubical type theory without an interval. In 21st International Conference on Types for Proofs and Programs LIPIcs Vol. 69 Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 3:1\u20133:27. DOI: 10.4230\/LIPIcs.TYPES.2015.3","DOI":"10.4230\/LIPIcs.TYPES.2015.3"},{"key":"e_1_3_3_7_2","unstructured":"Abhishek Anand and Greg Morrisett. 2017. Revisiting parametricity: Inductives and uniformity of propositions. arXiv:1705.01163. Retrieved from http:\/\/arxiv.org\/abs\/1705.01163"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00175-4"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45315-6_4","volume-title":"Foundations of Software Science and Computation Structures","author":"Barthe Gilles","year":"2001","unstructured":"Gilles Barthe and Olivier Pons. 2001. Type isomorphisms and proof reuse in dependent type theory. In Foundations of Software Science and Computation Structures. Furio Honsell and Marino Miculan (Eds.). Springer, Berlin, 57\u201371."},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_8"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","unstructured":"Sandrine Blazy. 2024. On mechanized semantics for verified compilation. Interview at the occasion of her invited talk at the ESOP 2024 Conference. Retrieved from https:\/\/etaps.org\/blog\/017-sandrine-blazy\/","DOI":"10.1007\/978-3-031-57259-3_1"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575676"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_11"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","unstructured":"Cyril Cohen Enzo Crance and Assia Mahboubi. 2025. rocq-community\/trocq: Trocq 0.1.8+prop. DOI: 10.5281\/zenodo.14846664","DOI":"10.5281\/zenodo.14846664"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.34"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_3_3_31_2","unstructured":"Thom Fr\u00fchwirth and Frank Raiser. 2011.\u00a0Constraint Handling Rules: Compilation Execution and Analysis. Retrieved from https:\/\/books.google.co.in\/books?id=BrH_wAEACAAJ"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_3_3_34_2","unstructured":"S\u00e9bastien Gou\u00ebzel. 2021. Vitali-Carath\u00e9odory theorem in mathlib. Retrieved from https:\/\/leanprover-community.github.io\/mathlib_docs\/measure_theory\/integral\/vitali_caratheodory.html"},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"Haftmann Florian","year":"2013","unstructured":"Florian Haftmann, Alexander Krauss, Ond\u0159ej Kun\u010dar, and Tobias Nipkow. 2013. Data Refinement in Isabelle\/HOL. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin|, 100\u2013115."},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.381"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2013.432"},{"key":"e_1_3_3_39_2","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"Lammich Peter","year":"2013","unstructured":"Peter Lammich. 2013. Automatic data refinement. In Interactive Theorem Proving. Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin, 84\u201399."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9461-9"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_13"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_6"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9350-4"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512669"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139567725"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_3_48_2","series-title":"Studies in Logic (Mathematical logic and foundations)","volume-title":"All About Proofs, Proofs for All","author":"Paulin-Mohring Christine","year":"2015","unstructured":"Christine Paulin-Mohring. 2015. Introduction to the calculus of inductive constructions. In All About Proofs, Proofs for All. Bruno Woltzenlogel Paleo and David Delahaye (Eds.), Studies in Logic (Mathematical logic and foundations), Vol. 55, College Publications. Retrieved from https:\/\/inria.hal.science\/hal-01094195"},{"key":"e_1_3_3_49_2","series-title":"Information Processing","first-page":"513","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In, Proceedings of the IFIP 9th World Computer Congress. R. E. A. Mason (Ed.), Information Processing, Vol. 83 North-Holland\/IFIP, 513\u2013523."},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1574"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.29"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. DOI: 10.5281\/zenodo.14542673","DOI":"10.5281\/zenodo.14542673"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2025. The Rocq Prover. DOI: 10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_3_3_58_2","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. Retrieved from https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632850"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_3_61_2","unstructured":"Cosmo Viola Max Fan and Talia Ringer. 2024. Proof repair across quotient type equivalences. Retrieved from https:\/\/arxiv.org\/abs\/2310.06959v5"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591224"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704900"},{"key":"e_1_3_3_65_2","volume-title":"Conference on Intelligent Computer Mathematics","author":"Zimmermann Th\u00e9o","year":"2015","unstructured":"Th\u00e9o Zimmermann and Hugo Herbelin. 2015. Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. In Conference on Intelligent Computer Mathematics. Retrieved from https:\/\/hal.science\/hal-01152588"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3737283","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T13:53:24Z","timestamp":1757944404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3737283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"references-count":64,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3737283"],"URL":"https:\/\/doi.org\/10.1145\/3737283","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"2024-04-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-19","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}