{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:21Z","timestamp":1767929481579,"version":"3.49.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2019-04545"],"award-info":[{"award-number":["2019-04545"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0053,FA9550-19-1-0216"],"award-info":[{"award-number":["FA9550-15-1-0053,FA9550-19-1-0216"]}],"id":[{"id":"10.13039\/100000181","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":[[2021,1,4]]},"abstract":"<jats:p>In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations.<\/jats:p>\n          <jats:p>In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.<\/jats:p>","DOI":"10.1145\/3434293","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Internalizing representation independence with univalence"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9590-3303","authenticated-orcid":false,"given":"Carlo","family":"Angiuli","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8174-7496","authenticated-orcid":false,"given":"Evan","family":"Cavallo","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Zeuner","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000155"},{"key":"e_1_2_1_2_1","unstructured":"Benedikt Ahrens and Peter LeFanu Lumsdaine. 2017. Displayed Categorie2sn.dInInternational Conference on Formal Structures for Computation and Deduction (FSCD 2017 ) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 84 ) (Eds.). Springer International Publishing Cham 160-17h6t.tps:\/\/doi.org\/10.1007\/978-3-319-08970-6_11  Benedikt Ahrens and Peter LeFanu Lumsdaine. 2017. Displayed Categorie2sn.dInInternational Conference on Formal Structures for Computation and Deduction (FSCD 2017 ) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 84 ) (Eds.). Springer International Publishing Cham 160-17h6t.tps:\/\/doi.org\/10.1007\/978-3-319-08970-6_11"},{"key":"e_1_2_1_3_1","unstructured":"Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom2. 1Inst International Conference on Types for Proofs and Programs (TYPES 2015 ) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 69 ) Tarmo Uustalu (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5 : 1-5 :34h.ttps:\/\/doi.org\/10.4230\/LIPIcs.TYPES. 2015.5  Cyril Cohen Thierry Coquand Simon Huber and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom2. 1Inst International Conference on Types for Proofs and Programs (TYPES 2015 ) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 69 ) Tarmo Uustalu (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl Germany 5 : 1-5 :34h.ttps:\/\/doi.org\/10.4230\/LIPIcs.TYPES. 2015.5"},{"key":"e_1_2_1_4_1","volume-title":"Refinements for Free!. ICnertified Programs and Proofs (CPP 2013 )","author":"Cohen Cyril"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2013.09.00I2nmemoryofN.G.(Dick)deBruijn(1918-2012"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009892"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_11"},{"key":"e_1_2_1_9_1","volume-title":"Germany), Amy P","author":"de Moura Leonardo"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_1_11_1","unstructured":"Edsger W. Dijkstra. 1974. On the role of scientific thought. (August 1974h)t.tps:\/\/www.cs.utexas.edu\/users\/EWD\/ transcriptions\/EWD04xx\/EWD447.html  Edsger W. Dijkstra. 1974. On the role of scientific thought. (August 1974h)t.tps:\/\/www.cs.utexas.edu\/users\/EWD\/ transcriptions\/EWD04xx\/EWD447.html"},{"key":"e_1_2_1_12_1","unstructured":"Mart\u00edn H\u00f6tzel Escard\u00f3. 2019. Introduction to univalent foundations of mathematics wihtthtApsg:d\/\/aw. ww.cs.bham.ac. uk\/~mhe\/ HoTT-UF-in-Agda-Lecture-Notes\/index.html  Mart\u00edn H\u00f6tzel Escard\u00f3. 2019. Introduction to univalent foundations of mathematics wihtthtApsg:d\/\/aw. ww.cs.bham.ac. uk\/~mhe\/ HoTT-UF-in-Agda-Lecture-Notes\/index.html"},{"key":"e_1_2_1_13_1","volume-title":"Three Equivalent Ordinal Notation Systems in Cubical Agda. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"Forsberg Fredrik Nordvall","year":"2020"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"Frumin Dan","year":"2018"},{"key":"e_1_2_1_15_1","volume-title":"Case Study: BatchedQueue. https:\/\/github.com\/limemloh\/CubicalAgdaBatchedQueue","author":"Gj\u00f8rup Emil","year":"2019"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004119000045"},{"key":"e_1_2_1_17_1","volume-title":"Interactive Theorem Proving (Rennes, France)(ITP 2013 ), Sandrine Blazy, Christine Paulin-Mohring","author":"Haftmann Florian"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003153"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00163-6"},{"key":"e_1_2_1_20_1","volume-title":"The law of excluded middle in the simplicial model of type tThehoreyory. and Applications of Categories 35, 40 (","author":"Kapulkin Chris","year":"2020"},{"key":"e_1_2_1_21_1","volume-title":"IAnCSL Annual Conference on Computer Science Logic (CSL 2012 ) (Leibniz International Proceedings in Informatics (LIPIcs)","volume":"16","author":"Keller Chantal","year":"2012"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:15)2017"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2013.432"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199476"},{"key":"e_1_2_1_26_1","volume-title":"\u201cbeta","author":"Licata Dan"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S030500411900015X"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_6"},{"key":"e_1_2_1_29_1","volume-title":"Changing Data Structures in Type Theory: A Study of Natural NumbTeyrps.esIn for Proofs and Programs (TYPES 2000 ) (Lecture Notes in Computer Science","author":"Magaud Nicolas"},{"key":"e_1_2_1_30_1","first-page":"71945","volume-title":"An Intuitionistic Theory of Types: Predicative Part. LIongic Colloquium '73","volume":"80","author":"Martin-L\u00f6f Per","year":"1975"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512669"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"e_1_2_1_35_1","first-page":"513","article-title":"Types, Abstraction and Parametric PolymorphismIn. fIonrmation Processing '83: Proceedings of the IFIP 9th World Computer Congress, R. E. A. Mason (Ed.)","author":"Reynolds John C.","year":"1983","journal-title":"North-Holland"},{"key":"e_1_2_1_36_1","volume-title":"Homotopy Type Theory. Master's thesis","author":"Rijke Egbert","year":"2012"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00126-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90023-7"},{"key":"e_1_2_1_40_1","unstructured":"hTomas Streicher. 1993. Investigations Into Intensional Type Theory. Habilitation thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen. https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf  hTomas Streicher. 1993. Investigations Into Intensional Type Theory. Habilitation thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen. https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_2_1_42_1","volume-title":"The Marriage of Univalence and Parametricity. arXiv","author":"Tabareau Nicolas","year":"1909"},{"key":"e_1_2_1_43_1","unstructured":"hTe Agda Development Team. 2020. The Agda Programming Language. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php  hTe Agda Development Team. 2020. The Agda Programming Language. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_2_1_44_1","unstructured":"hTe Coq Development Team. 2020. The Coq Proof Assistant. https:\/\/www.coq.inria.fr  hTe Coq Development Team. 2020. The Coq Proof Assistant. https:\/\/www.coq.inria.fr"},{"key":"e_1_2_1_45_1","unstructured":"hTe Mathematical Components Team. 2020. The Mathematical Components libraryh.ttps:\/\/github.com\/math-comp\/mathcomp  hTe Mathematical Components Team. 2020. The Mathematical Components libraryh.ttps:\/\/github.com\/math-comp\/mathcomp"},{"key":"e_1_2_1_46_1","volume-title":"Miranda: A non-strict functional language with polymorphic tyFpuensc. tiIonnal Programming Languages and Computer Architecture (FPCA 1985 ), Jean-Pierre Jouannaud (Ed.)","author":"Turner D. A.","year":"1985"},{"key":"e_1_2_1_47_1","unstructured":"hTe Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published. https:\/\/homotopytypetheory.org\/book\/  hTe Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_2_1_48_1","volume-title":"Brazil( ) ITP 2017 ), Mauricio Ayala-Rinc\u00f3n and C\u00e9sar A","author":"van Doorn Floris"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_1_50_1","unstructured":"Vladimir Voevodsky. 2010a. The equivalence axiom and univalent models of type theoryh. ttp:\/\/www.math.ias.edu\/ vladimir\/files\/CMU_talk. pdNfotes from a talk at Carnegie Mellon University.  Vladimir Voevodsky. 2010a. The equivalence axiom and univalent models of type theoryh. ttp:\/\/www.math.ias.edu\/ vladimir\/files\/CMU_talk. pdNfotes from a talk at Carnegie Mellon University."},{"key":"e_1_2_1_51_1","unstructured":"Vladimir Voevodsky. 2010b. Univalent Foundationhst.tps:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/ Bonn_talk. pdNfotes from a talk in Bonn.  Vladimir Voevodsky. 2010b. Univalent Foundationhst.tps:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/ Bonn_talk. pdNfotes from a talk in Bonn."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"},{"key":"e_1_2_1_53_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens Daniel Grayson etal 2020. UniMath-a computer-checked library of univalent mathematics. https:\/\/github.com\/UniMath\/UniMath  Vladimir Voevodsky Benedikt Ahrens Daniel Grayson et al. 2020. UniMath-a computer-checked library of univalent mathematics. https:\/\/github.com\/UniMath\/UniMath"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_55_1","unstructured":"James Wood. 2019. Vectors and Matrices in Agda. Blog poshttattps:\/\/personal.cis.strath.ac.uk\/james.wood.100\/blog\/html\/ VecMat.htm.l  James Wood. 2019. Vectors and Matrices in Agda. Blog poshttattps:\/\/personal.cis.strath.ac.uk\/james.wood.100\/blog\/html\/ VecMat.htm.l"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434293","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434293","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434293"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434293"],"URL":"https:\/\/doi.org\/10.1145\/3434293","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}