{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:11:42Z","timestamp":1781853102594,"version":"3.54.5"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["Starting Grant CoqHoTT 637339"],"award-info":[{"award-number":["Starting Grant CoqHoTT 637339"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002848","name":"Comisi\u00f3n Nacional de Investigaci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["Fondecyt Regular 1150017 & Redes 170067"],"award-info":[{"award-number":["Fondecyt Regular 1150017 & Redes 170067"]}],"id":[{"id":"10.13039\/501100002848","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. We present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. Our approach handles both type and term dependency. We study how to maximize the effectiveness of these transports in terms of computational behavior, and identify a fragment useful for certified programming on which univalent transport is guaranteed to be effective. This work paves the way to easier-to-use environments for certified programming by supporting seamless programming and proving modulo equivalences.<\/jats:p>","DOI":"10.1145\/3236787","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Equivalences for free: univalent parametricity for effective transport"],"prefix":"10.1145","volume":"2","author":[{"given":"Nicolas","family":"Tabareau","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Inria, France \/ IRIF, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Leibniz International Proceedings in Informatics.","author":"Altenkirch Thorsten","year":"2017","unstructured":"Thorsten Altenkirch and Ambrus Kaposi . 2017 . Towards a cubical type theory without an interval . Leibniz International Proceedings in Informatics. Thorsten Altenkirch and Ambrus Kaposi. 2017. Towards a cubical type theory without an interval. Leibniz International Proceedings in Informatics."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_1_3_1","volume-title":"Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand and Greg Morrisett . 2017 . Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163 (2017). http:\/\/arxiv.org\/abs\/1705.01163 Abhishek Anand and Greg Morrisett. 2017. Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163 (2017). http:\/\/arxiv.org\/abs\/1705.01163"},{"key":"e_1_2_1_4_1","first-page":"66","article-title":"The Untenability of Genera","volume":"17","author":"Bacon John","year":"1974","unstructured":"John Bacon . 1974 . The Untenability of Genera . Logique et Analyse 17 , 65\/ 66 (jan-apr 1974), 197\u2013208. John Bacon. 1974. The Untenability of Genera. Logique et Analyse 17, 65\/66 (jan-apr 1974), 197\u2013208.","journal-title":"Logique et Analyse"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_1_9_1","volume-title":"Cubical Type Theory: a constructive interpretation of the univalence axiom. (Oct","author":"Cohen Cyril","year":"2016","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2016. Cubical Type Theory: a constructive interpretation of the univalence axiom. (Oct . 2016 ). https:\/\/hal.inria.fr\/hal- 01378906 Accepted for publication in LIPIcs . Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2016. Cubical Type Theory: a constructive interpretation of the univalence axiom. (Oct. 2016). https:\/\/hal.inria.fr\/hal- 01378906 Accepted for publication in LIPIcs."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_2_1_11_1","unstructured":"The Coq Development Team. 2016. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.6.  The Coq Development Team. 2016. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.6."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Conference for Computer Science Logic (CSL","author":"Neelakantan","year":"2013","unstructured":"Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions . In Proceedings of the Conference for Computer Science Logic (CSL 2013 ). 432\u2013451. Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In Proceedings of the Conference for Computer Science Logic (CSL 2013). 432\u2013451."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_6"},{"key":"e_1_2_1_18_1","volume-title":"Changing Data Structures in Type Theory: A Study of Natural Numbers. In International Workshop on Types for Proofs and Programs (TYPES 2000)","volume":"2277","author":"Magaud Nicolas","year":"2000","unstructured":"Nicolas Magaud and Yves Bertot . 2000 . Changing Data Structures in Type Theory: A Study of Natural Numbers. In International Workshop on Types for Proofs and Programs (TYPES 2000) (Lecture Notes in Computer Science), P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (Eds.) , Vol. 2277 . Springer-Verlag, 181\u2013196. Nicolas Magaud and Yves Bertot. 2000. Changing Data Structures in Type Theory: A Study of Natural Numbers. In International Workshop on Types for Proofs and Programs (TYPES 2000) (Lecture Notes in Computer Science), P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (Eds.), Vol. 2277. Springer-Verlag, 181\u2013196."},{"key":"e_1_2_1_19_1","unstructured":"Per Martin-L\u00f6f. 1971. An Intuitionistic Theory of Types. Unpublished manuscript.  Per Martin-L\u00f6f. 1971. An Intuitionistic Theory of Types. Unpublished manuscript."},{"key":"e_1_2_1_20_1","volume-title":"All about Proofs, Proofs for All, Bruno Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations)","author":"Paulin-Mohring Christine","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 . 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."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_1_22_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types , Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523 . John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_1_24_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_26_1","unstructured":"Theo Zimmermann and Hugo Herbelin. 2015. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. arXiv:1505.05028v4.  Theo Zimmermann and Hugo Herbelin. 2015. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. arXiv:1505.05028v4."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236787","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":26,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236787"],"URL":"https:\/\/doi.org\/10.1145\/3236787","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}