{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:17Z","timestamp":1767929477859,"version":"3.49.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,15]],"date-time":"2021-01-15T00:00:00Z","timestamp":1610668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ANID FONDECYT Regular Project","award":["1190058"],"award-info":[{"award-number":["1190058"]}]},{"name":"ANID\/CONICYT REDES Project","award":["170067"],"award-info":[{"award-number":["170067"]}]},{"name":"ERC Starting","award":["CoqHoTT 637339"],"award-info":[{"award-number":["CoqHoTT 637339"]}]},{"name":"Inria \u00c9quipe Associ\u00e9e GECO"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2021,2,28]]},"abstract":"<jats:p>\n            Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called\n            <jats:italic>univalent parametricity<\/jats:italic>\n            , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, 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. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports\n            <jats:italic>transport \u00e0 la carte<\/jats:italic>\n            : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.\n          <\/jats:p>","DOI":"10.1145\/3429979","type":"journal-article","created":{"date-parts":[[2021,1,15]],"date-time":"2021-01-15T23:06:41Z","timestamp":1610752001000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["The Marriage of Univalence and Parametricity"],"prefix":"10.1145","volume":"68","author":[{"given":"Nicolas","family":"Tabareau","sequence":"first","affiliation":[{"name":"Gallinette Project-Team, Inria, Nantes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"Computer Science Department (DCC), University of Chile, Santiago, RM, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"Gallinette Project-Team, Inria, Nantes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,15]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES\u201915)","volume":"69","author":"Altenkirch Thorsten","year":"2015","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 (TYPES\u201915) , Tarmo Uustalu (Ed.) , Vol. 69 . LIPICS. Thorsten Altenkirch and Ambrus Kaposi. 2015. Towards a cubical type theory without an interval. In 21st International Conference on Types for Proofs and Programs (TYPES\u201915), Tarmo Uustalu (Ed.), Vol. 69. LIPICS."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Conor McBride and Wouter Swierstra. 2007. Observational equality now! In Proceedings of the Workshop on Programming Languages meets Program Verification (PLPV\u201907). 57--68.  Thorsten Altenkirch Conor McBride and Wouter Swierstra. 2007. Observational equality now! In Proceedings of the Workshop on Programming Languages meets Program Verification (PLPV\u201907). 57--68.","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 ). Abhishek Anand and Greg Morrisett. 2017. Revisiting parametricity: Inductives and uniformity of propositions. CoRR abs\/1705.01163 (2017)."},{"key":"e_1_2_1_4_1","volume-title":"27th EACSL Annual Conference on Computer Science Logic (CSL\u201918)","author":"Angiuli Carlo","year":"2018","unstructured":"Carlo Angiuli , Kuen-Bang Hou , and Robert Harper . 2018 . Cartesian cubical computational type theory: Constructive reasoning with paths and equalities . In 27th EACSL Annual Conference on Computer Science Logic (CSL\u201918) . 6:1--6:17. Carlo Angiuli, Kuen-Bang Hou, and Robert Harper. 2018. Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL\u201918). 6:1--6:17."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Simon Boulier Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2017. The next 700 syntactical models of type theory. In Certified Programs and Proofs (CPP\u201917). 182--194.  Simon Boulier Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2017. The next 700 syntactical models of type theory. In Certified Programs and Proofs (CPP\u201917). 182--194.","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_1_10_1","volume-title":"28th EACSL Annual Conference on Computer Science Logic (CSL'20)","author":"Cavallo Evan","year":"2020","unstructured":"Evan Cavallo and Robert Harper . 2020 . Internal parametricity for Cubical Type Theory . In 28th EACSL Annual Conference on Computer Science Logic (CSL'20) . 13:1--13:17 pages. Evan Cavallo and Robert Harper. 2020. Internal parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL'20). 13:1--13:17 pages."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES'15)","author":"Cohen Cyril","year":"2015","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2015 . Cubical Type Theory: A constructive interpretation of the univalence axiom . In Proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES'15) . 5:1--5:34 pages. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2015. Cubical Type Theory: A constructive interpretation of the univalence axiom. In Proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES'15). 5:1--5:34 pages."},{"key":"e_1_2_1_12_1","volume-title":"Refinements for free! In Proceedings of the International Conference on Certified Programming and Proofs (CPP\u201913) (Lecture Notes in Computer Science)","author":"Cohen Cyril","unstructured":"Cyril Cohen , Maxime D\u00e9n\u00e8s , and Anders M\u00f6rtberg . 2013. Refinements for free! In Proceedings of the International Conference on Certified Programming and Proofs (CPP\u201913) (Lecture Notes in Computer Science) , G. Gonthier and M. Norrish (Eds.), Vol. 8307 . Springer-Verlag , 147--162. Cyril Cohen, Maxime D\u00e9n\u00e8s, and Anders M\u00f6rtberg. 2013. Refinements for free! In Proceedings of the International Conference on Certified Programming and Proofs (CPP\u201913) (Lecture Notes in Computer Science), G. Gonthier and M. Norrish (Eds.), Vol. 8307. Springer-Verlag, 147--162."},{"key":"#cr-split#-e_1_2_1_13_1.1","unstructured":"Coq Development Team. 2020. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.1003420. 10.5281\/zenodo.1003420"},{"key":"#cr-split#-e_1_2_1_13_1.2","unstructured":"Coq Development Team. 2020. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.1003420."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000069"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"e_1_2_1_17_1","volume-title":"Eliminating Dependent Pattern Matching","author":"Goguen Healfdene","unstructured":"Healfdene Goguen , Conor McBride , and James McKinna . 2006. Eliminating Dependent Pattern Matching . Springer Berlin Heidelberg , Berlin ,521--540. Healfdene Goguen, Conor McBride, and James McKinna. 2006. Eliminating Dependent Pattern Matching. Springer Berlin Heidelberg, Berlin,521--540."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003153"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_2_1_21_1","volume-title":"Homotopical inverse diagrams in categories with attributes. arXiv preprint arXiv:1808.01816","author":"Kapulkin Chris","year":"2018","unstructured":"Chris Kapulkin and Peter LeFanu Lumsdaine . 2018. Homotopical inverse diagrams in categories with attributes. arXiv preprint arXiv:1808.01816 ( 2018 ). Chris Kapulkin and Peter LeFanu Lumsdaine. 2018. Homotopical inverse diagrams in categories with attributes. arXiv preprint arXiv:1808.01816 (2018)."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the Conference for Computer Science Logic (CSL\u201913)","author":"Neelakantan","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\u201913) . 432--451. 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\u201913). 432--451."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_6"},{"key":"e_1_2_1_25_1","volume-title":"International Workshop on Types for Proofs and Programs (TYPES\u201900)","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\u201900) (Lecture Notes in Computer Science), P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (Eds.) , Vol. 2277 . Springer-Verlag, 181--196. 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\u201900) (Lecture Notes in Computer Science), P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (Eds.), Vol. 2277. Springer-Verlag, 181--196."},{"key":"e_1_2_1_26_1","volume-title":"Logic Colloquium\u201973","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f . 1975. An intuitionistic theory of types: Predicative part . In Logic Colloquium\u201973 , H. E. Rose and J. C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80 . Elsevier , 73--118. Per Martin-L\u00f6f. 1975. An intuitionistic theory of types: Predicative part. In Logic Colloquium\u201973, H. E. Rose and J. C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 73--118."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_2_1_29_1","volume-title":"Studies in Logic (Mathematical Logic and Foundations)","volume":"55","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 . 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_30_1","volume-title":"Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming (ICFP\u201906)","author":"Jones Simon Peyton","year":"2006","unstructured":"Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , and Geoffrey Washburn . 2006 . Simple unification-based type inference for GADTs . In Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming (ICFP\u201906) . ACM Press, Portland, Oregon, 50--61. Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type inference for GADTs. In Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming (ICFP\u201906). ACM Press, Portland, Oregon, 50--61."},{"key":"e_1_2_1_31_1","volume-title":"IFIP Congress. 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types, abstraction and parametric polymorphism . In IFIP Congress. 513--523 . John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In IFIP Congress. 513--523."},{"key":"e_1_2_1_32_1","volume-title":"10th International Conference on Interactive Theorem Proving (ITP\u201919)","volume":"141","author":"Ringer Talia","year":"2019","unstructured":"Talia Ringer , Nathaniel Yazdani , John Leo , and Dan Grossman . 2019 . Ornaments for proof reuse in Coq . In 10th International Conference on Interactive Theorem Proving (ITP\u201919) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O\u2019Leary, and Andrew Tolmach (Eds.) , Vol. 141 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 26:1--26:19. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2019. Ornaments for proof reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP\u201919) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O\u2019Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 26:1--26:19."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00126-4"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_2_1_38_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Program Univalent Foundations","unstructured":"Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_1_40_1","unstructured":"Vladimir Voevodsky. 2010. The Equivalence Axiom and Univalent Models of Type Theory. arXiv:1402.5556.  Vladimir Voevodsky. 2010. The Equivalence Axiom and Univalent Models of Type Theory. arXiv:1402.5556."},{"key":"e_1_2_1_41_1","volume-title":"Theorems for free! In Functional Programming Languages and Computer Architecture","author":"Wadler Philip","unstructured":"Philip Wadler . 1989. Theorems for free! In Functional Programming Languages and Computer Architecture . ACM Press , 347--359. Philip Wadler. 1989. Theorems for free! In Functional Programming Languages and Computer Architecture. ACM Press, 347--359."},{"key":"e_1_2_1_42_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":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3429979","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3429979","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:46Z","timestamp":1750195906000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3429979"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,15]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,2,28]]}},"alternative-id":["10.1145\/3429979"],"URL":"https:\/\/doi.org\/10.1145\/3429979","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,15]]},"assertion":[{"value":"2019-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}