{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:38:40Z","timestamp":1768163920143,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572616","type":"print"},{"value":"9783031572623","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This article presents <jats:sc>Trocq<\/jats:sc>, a new proof transfer framework for dependent type theory. <jats:sc>Trocq<\/jats:sc> 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.<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_10","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"239-268","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Trocq: Proof Transfer for Free, With or Without Univalence"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3540-1050","authenticated-orcid":false,"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0498-0910","authenticated-orcid":false,"given":"Enzo","family":"Crance","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0312-5461","authenticated-orcid":false,"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"The lean mathematical library. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. pp. 367\u2013381. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373824, https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Cohen, C.: Measure construction by extension in dependent type theory with application to integration (2023), accepted for publication in JAR","DOI":"10.1007\/s10817-023-09671-5"},{"key":"10_CR3","unstructured":"Altenkirch, T., Kaposi, A.: Towards a cubical type theory without an interval. In: TYPES. LIPIcs, vol.\u00a069, pp. 3:1\u20133:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Angiuli, C., Brunerie, G., Coquand, T., Harper, R., (Favonia), K.H., Licata, D.R.: Syntax and models of cartesian cubical type theory. Math. Struct. Comput. Sci. 31(4), 424\u2013468 (2021). https:\/\/doi.org\/10.1017\/S0960129521000347, https:\/\/doi.org\/10.1017\/S0960129521000347","DOI":"10.1017\/S0960129521000347"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Angiuli, C., Cavallo, E., M\u00f6rtberg, A., Zeuner, M.: Internalizing representation independence with univalence. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434293, https:\/\/doi.org\/10.1145\/3434293","DOI":"10.1145\/3434293"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Aspinall, D., Compagnoni, A.B.: Subtyping dependent types. Theor. Comput. Sci. 266(1-2), 273\u2013309 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00175-4, https:\/\/doi.org\/10.1016\/S0304-3975(00)00175-4","DOI":"10.1016\/S0304-3975(00)00175-4"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003). https:\/\/doi.org\/10.1017\/S0956796802004501, https:\/\/doi.org\/10.1017\/S0956796802004501","DOI":"10.1017\/S0956796802004501"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The hott library: a formalization of homotopy type theory in coq. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pp. 164\u2013172. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018615, https:\/\/doi.org\/10.1145\/3018610.3018615","DOI":"10.1145\/3018610.3018615"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Jansson, P., Paterson, R.: Proofs for free - parametricity for dependent types. J. Funct. Program. 22(2), 107\u2013152 (2012). https:\/\/doi.org\/10.1017\/S0956796812000056, https:\/\/doi.org\/10.1017\/S0956796812000056","DOI":"10.1017\/S0956796812000056"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Lasson, M.: Realizability and parametricity in pure type systems. In: Hofmann, M. (ed.) Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06604, pp. 108\u2013122. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_8, https:\/\/doi.org\/10.1007\/978-3-642-19805-2_8","DOI":"10.1007\/978-3-642-19805-2_8"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Boulier, S., P\u00e9drot, P., Tabareau, N.: The next 700 syntactical models of type theory. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pp. 182\u2013194. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018620, https:\/\/doi.org\/10.1145\/3018610.3018620","DOI":"10.1145\/3018610.3018620"},{"key":"10_CR12","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: A constructive interpretation of the univalence axiom. FLAP 4(10), 3127\u20133170 (2017), http:\/\/collegepublications.co.uk\/ifcolog\/?00019"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Cohen, C., Crance, E., Mahboubi, A.: coq-community\/trocq: Trocq 0.1.5 (Jan 2024). https:\/\/doi.org\/10.5281\/zenodo.10563382, https:\/\/doi.org\/10.5281\/zenodo.10563382","DOI":"10.5281\/zenodo.10563382"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Lecture Notes in Computer Science, vol.\u00a08307, pp. 147\u2013162. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_10, https:\/\/doi.org\/10.1007\/978-3-319-03545-1_10","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3, https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in coq. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving. pp. 83\u201398. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09450, pp. 460\u2013468. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32, https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"10_CR18","unstructured":"Gou\u00ebzel, S.: Vitali-carath\u00e9odory theorem in mathlib. https:\/\/leanprover-community.github.io\/mathlib_docs\/measure_theory\/integral\/vitali_caratheodory.html (2021)"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Keller, C., Lasson, M.: Parametricity in an impredicative sort. In: C\u00e9gielski, P., Durand, A. (eds.) Computer Science Logic (CSL\u201912) - 26th International Workshop\/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France. LIPIcs, vol.\u00a016, pp. 381\u2013395. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.381, https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.381","DOI":"10.4230\/LIPIcs.CSL.2012.381"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in coq. J. Autom. Reason. 57(3), 187\u2013217 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9350-4, https:\/\/doi.org\/10.1007\/s10817-015-9350-4","DOI":"10.1007\/s10817-015-9350-4"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Mitchell, J.C.: Representation independence and data abstraction. In: Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986. pp. 263\u2013276. ACM Press (1986). https:\/\/doi.org\/10.1145\/512644.512669, https:\/\/doi.org\/10.1145\/512644.512669","DOI":"10.1145\/512644.512669"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12699, pp. 625\u2013635. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37, https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Nederpelt, R., Geuvers, H.: Type Theory and Formal Proof: An Introduction. Cambridge University Press (2014). https:\/\/doi.org\/10.1017\/CBO9781139567725","DOI":"10.1017\/CBO9781139567725"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Norell, U.: Dependently typed programming in agda. In: Koopman, P.W.M., Plasmeijer, R., Swierstra, S.D. (eds.) Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures. Lecture Notes in Computer Science, vol.\u00a05832, pp. 230\u2013266. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5, https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"10_CR25","unstructured":"Paulin-Mohring, C.: Introduction to the Calculus of Inductive Constructions. In: Paleo, B.W., Delahaye, D. (eds.) All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations), vol.\u00a055. College Publications (Jan 2015), https:\/\/inria.hal.science\/hal-01094195"},{"key":"10_CR26","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983. pp. 513\u2013523. North-Holland\/IFIP (1983)"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Ringer, T., Porter, R., Yazdani, N., Leo, J., Grossman, D.: Proof repair across type equivalences. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 112\u2013127. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454033, https:\/\/doi.org\/10.1145\/3453483.3454033","DOI":"10.1145\/3453483.3454033"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formaliz. Reason. 2(1), 41\u201362 (2009). https:\/\/doi.org\/10.6092\/issn.1972-5787\/1574, https:\/\/doi.org\/10.6092\/issn.1972-5787\/1574","DOI":"10.6092\/issn.1972-5787\/1574"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Tabareau, N., Tanter, \u00c9., Sozeau, M.: Equivalences for free: univalent parametricity for effective transport. Proceedings of the ACM on Programming Languages 2(ICFP), 1\u201329 (2018)","DOI":"10.1145\/3236787"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Tabareau, N., Tanter, \u00c9., Sozeau, M.: The marriage of univalence and parametricity. Journal of the ACM (JACM) 68(1), 1\u201344 (2021)","DOI":"10.1145\/3429979"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Tassi, E.: Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. In: ITP 2019 - 10th International Conference on Interactive Theorem Proving. Portland, United States (Sep 2019). https:\/\/doi.org\/10.4230\/LIPIcs.CVIT.2016.23, https:\/\/inria.hal.science\/hal-01897468","DOI":"10.4230\/LIPIcs.CVIT.2016.23"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The coq proof assistant (Sep 2022). https:\/\/doi.org\/10.5281\/zenodo.7313584, https:\/\/doi.org\/10.5281\/zenodo.7313584","DOI":"10.5281\/zenodo.7313584"},{"key":"10_CR33","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Vezzosi, A., M\u00f6rtberg, A., Abel, A.: Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. 3(ICFP), 87:1\u201387:29 (2019). https:\/\/doi.org\/10.1145\/3341691, https:\/\/doi.org\/10.1145\/3341691","DOI":"10.1145\/3341691"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Theorems for free! In: Stoy, J.E. (ed.) Proceedings of the fourth international conference on Functional programming languages and computer architecture, FPCA 1989, London, UK, September 11-13, 1989. pp. 347\u2013359. ACM (1989). https:\/\/doi.org\/10.1145\/99370.99404, https:\/\/doi.org\/10.1145\/99370.99404","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57262-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:04:15Z","timestamp":1712214255000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"None.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}