{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:12:38Z","timestamp":1751688758712,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Two approaches exist to incorporate parametricity into proof assistants based on dependent type theory. On the one hand, parametricity translations conveniently compute parametricity statements and their proofs solely based on individual well-typed polymorphic programs. But they do not offer internal parametricity: formal proofs that any polymorphic program of a certain type satisfies its parametricity statement. On the other hand, internally parametric type theories augment plain type theory with additional primitives out of which internal parametricity can be derived. But those type theories lack mature proof assistant implementations and deriving parametricity in them involves low-level intractable proofs. In this paper, we contribute Agda --bridges: the first practical internally parametric proof assistant. We provide the first mechanized proofs of crucial theorems for internal parametricity, like the relativity theorem. We identify a high-level sufficient condition for proving internal parametricity which we call the structure relatedness principle (SRP) by analogy with the structure identity principle (SIP) of HoTT\/UF. We state and prove a general parametricity theorem for types that satisfy the SRP. Our parametricity theorem lets us obtain one-liner proofs of standard internal free theorems. We observe that the SRP is harder to prove than the SIP and provide in Agda --bridges a shallowly embedded type theory to compose types that satisfy the SRP. This type theory is an observational type theory of logical relations and our parametricity theorem ought to be one of its inference rules.<\/jats:p>","DOI":"10.1145\/3632850","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"209-240","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Internal and Observational Parametricity for Cubical Agda"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4144-9368","authenticated-orcid":false,"given":"Antoine","family":"Van Muylder","sequence":"first","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1571-5063","authenticated-orcid":false,"given":"Andreas","family":"Nuyts","sequence":"additional","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90082-5"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2005.06.002"},{"key":"e_1_3_1_4_1","unstructured":"The Agda Community. [n. d.]. A standard library for Cubical Agda. https:\/\/github.com\/agda\/cubical"},{"key":"e_1_3_1_5_1","unstructured":"Agda Development Team. 2023. Agda 2.6.3 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.3\/"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:20)2019"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394755"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632920"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2015.3"},{"key":"e_1_3_1_10_1","volume-title":"28th International Conference on Types for Proofs and Programs (TYPES 2022)","author":"Altenkirch Thorsten","year":"2022","unstructured":"Thorsten Altenkirch, Ambrus Kaposi, and Michael Shulman. 2022. Towards Higher Observational Type Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_1_12_1","unstructured":"Abhishek Anand and Greg Morrisett. 2017. Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs\/1705.01163 (2017). arXiv:1705.01163 http:\/\/arxiv.org\/abs\/1705.01163"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2018.6"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2012.46"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209130"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0014043"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.006"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2016.7"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_1_25_1","unstructured":"Evan Cavallo. 2020. Ptt an experimental implementation of Martin-L\u00f6f type theory with n-ary internal parametricity. https:\/\/github.com\/ecavallo\/ptt"},{"key":"e_1_3_1_26_1","unstructured":"Evan Cavallo and Robert Harper. 2019. Parametric Cubical Type Theory. CoRR abs\/1901.00489 (2019). arXiv:1901.00489 http:\/\/arxiv.org\/abs\/1901.00489"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(4:5)2021"},{"issue":"10","key":"e_1_3_1_28_1","first-page":"3127","article-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom","volume":"4","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2017. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4, 10 (2017), 3127\u20133170. http:\/\/collegepublications.co.uk\/ifcolog\/?00019","journal-title":"FLAP"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"e_1_3_1_30_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d'ordre sup\u00e9rieur. Ph. D. Dissertation. \u00c9diteur inconnu."},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2014.02.008"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2012.381"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2013.432"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/08905401(91)90053-5"},{"key":"e_1_3_1_35_1","unstructured":"Michael Makkai. 1995. First order logic with dependent sorts with applications to category theory. (1995). http:\/\/www.math.mcgill.ca\/makkai\/folds\/foldsinpdf\/FOLDS.pdf"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2018.23"},{"key":"e_1_3_1_37_1","volume-title":"Internalizing Parametricity","author":"Moulin Guilhem","year":"2016","unstructured":"Guilhem Moulin. 2016. Internalizing Parametricity. Ph. D. Dissertation. Chalmers University of Technology, Gothenburg, Sweden. http:\/\/publications.lib.chalmers.se\/publication\/235758-internalizing-parametricity"},{"key":"e_1_3_1_38_1","unstructured":"Andreas Nuyts. 2021. Parametricity Features and their Requirements. CoRR abs\/2111.09822 (2021). arXiv:2111.09822 https:\/\/arxiv.org\/abs\/2111.09822"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0037118"},{"key":"e_1_3_1_42_1","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. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_3_1_45_1","first-page":"513","volume-title":"Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R. E. A. Mason (Ed.). North-Holland\/IFIP, 513\u2013523."},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"e_1_3_1_47_1","unstructured":"Egbert Rijke. 2022. Introduction to Homotopy Type Theory. arXiv:2212.11082 [math.LO]"},{"key":"e_1_3_1_48_1","volume-title":"28th International Conference on Types for Proofs and Programs (TYPES 2022)","author":"Rose Robert","year":"2022","unstructured":"Robert Rose, Matthew Z Weaver, and Daniel R Licata. 2022. Deciding the cofibration logic of cartesian cubical type theories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_3_1_50_1","volume-title":"Technical report 1217","author":"Takeuti Izumi","year":"2001","unstructured":"Izumi Takeuti. 2001. The Theory of Parametricity in Lambda Cube. Technical report 1217, Kyoto University. https:\/\/repository.kulib.kyoto-u.ac.jp\/dspace\/bitstream\/2433\/41237\/1\/1217_10.pdf"},{"key":"e_1_3_1_51_1","unstructured":"The Coq development team. 2022. The Coq proof assistant. http:\/\/coq.inria.fr"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Antoine Van Muylder Andreas Nuyts and Dominique Devriese. 2023. Agda --bridges VM. https:\/\/doi.org\/10.5281\/zenodo.10009365 10.5281\/zenodo.10009365","DOI":"10.5281\/zenodo.10009365"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373814"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2022.100846"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.12.042"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632850","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:48Z","timestamp":1751659488000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632850"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632850"],"URL":"https:\/\/doi.org\/10.1145\/3632850","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}