{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T03:56:20Z","timestamp":1784001380197,"version":"3.55.0"},"reference-count":34,"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\/"}],"funder":[{"name":"Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund","award":["TKP2021-NVA"],"award-info":[{"award-number":["TKP2021-NVA"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0009"],"award-info":[{"award-number":["FA9550-21-1-0009"]}],"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":[[2024,1,2]]},"abstract":"<jats:p>Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-L\u00f6f type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.<\/jats:p>","DOI":"10.1145\/3632920","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2340-2369","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Internal Parametricity, without an Interval"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6582-5025","authenticated-orcid":false,"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2689-9148","authenticated-orcid":false,"given":"Yorgo","family":"Chamoun","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9897-8936","authenticated-orcid":false,"given":"Ambrus","family":"Kaposi","sequence":"additional","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9948-6682","authenticated-orcid":false,"given":"Michael","family":"Shulman","sequence":"additional","affiliation":[{"name":"University of San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.21"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.3"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_1_6_1","volume-title":"CoRR","author":"Annenkov Danil","year":"2017","unstructured":"Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. CoRR abs\/1705.03307 (2017). arXiv:1705.03307 http:\/\/arxiv.org\/abs\/1705.03307"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500577"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2023.18"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2016.7"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57418-9_5"},{"key":"e_1_3_1_16_1","article-title":"Categories with Families: Unityped, Simply Typed, and Dependently Typed","author":"Castellan Simon","year":"2019","unstructured":"Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2019. Categories with Families: Unityped, Simply Typed, and Dependently Typed. CoRR abs\/1904.00827 (2019). arXiv:1904.00827 http:\/\/arxiv.org\/abs\/1904.00827","journal-title":"CoRR"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1184\/r1\/14555691"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(4:5)2021"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2015.5"},{"key":"e_1_3_1_20_1","unstructured":"Thierry Coquand. 2018. Presheaf model of type theory. (2018). https:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.11842"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394770"},{"key":"e_1_3_1_27_1","article-title":"Space-Valued Diagrams, Type-Theoretically (Extended Abstract)","author":"Kraus Nicolai","year":"2017","unstructured":"Nicolai Kraus and Christian Sattler. 2017. Space-Valued Diagrams, Type-Theoretically (Extended Abstract). CoRR abs\/1704.04543 (2017). arXiv:1704.04543 http:\/\/arxiv.org\/abs\/1704.04543","journal-title":"CoRR"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632850"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_1_31_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_32_1","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling. 2022. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University USA. https:\/\/doi.org\/10.1184\/r1\/19632681.v1 10.1184\/r1\/19632681.v1","DOI":"10.1184\/r1\/19632681.v1"},{"key":"e_1_3_1_33_1","article-title":"A General Framework for the Semantics of Type Theory","author":"Uemura Taichi","year":"2019","unstructured":"Taichi Uemura. 2019. A General Framework for the Semantics of Type Theory. CoRR abs\/1904.04097 (2019). arXiv:1904.04097 http:\/\/arxiv.org\/abs\/1904.04097","journal-title":"CoRR abs\/1904.04097"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"e_1_3_1_35_1","unstructured":"Philip Wadler. 1990. Recursive types for free! (1990). https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632920","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632920","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632920","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:58Z","timestamp":1751659558000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632920"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632920"],"URL":"https:\/\/doi.org\/10.1145\/3632920","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}