{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:19:28Z","timestamp":1770290368556,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,8,29]]},"abstract":"<jats:p>Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically in Reynolds's theory of relational parametricity, which allows the metatheoretical derivation of parametricity theorems about all values of a given type. Although predicative System F embeds into dependent type systems such as Martin-L\u00f6f Type Theory (MLTT), parametricity does not carry over as easily. The identity extension lemma, which is crucial if we want to prove theorems involving equality, has only been shown to hold for small types, excluding the universe.<\/jats:p>\n          <jats:p>We attribute this to the fact that MLTT uses a single type former \u03a0 to generalize both the parametric quantifier \u2200 and the type former \u2192 which is non-parametric in the sense that its elements may use their argument as a value. We equip MLTT with parametric quantifiers \u2200 and \u2203 alongside the existing \u03a0 and \u03a3, and provide relation type formers for proving parametricity theorems internally. We show internally the existence of initial algebras and final co-algebras of indexed functors both by Church encoding and, for a large class of functors, by using sized types.<\/jats:p>\n          <jats:p>We prove soundness of our type system by enhancing existing iterated reflexive graph (cubical set) models of dependently typed parametricity by distinguishing between edges that express relatedness of objects (bridges) and edges that express equality (paths). The parametric functions are those that map bridges to paths.<\/jats:p>\n          <jats:p>We implement an extension to the Agda proof assistant that type-checks proofs in our type system.<\/jats:p>","DOI":"10.1145\/3110276","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Parametric quantifiers for dependent type theory"],"prefix":"10.1145","volume":"1","author":[{"given":"Andreas","family":"Nuyts","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90082-5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006853"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_2_2_6_1","volume-title":"Extending Homotopy Type Theory with Strict Equality. CoRR abs\/1604.03799","author":"Altenkirch Thorsten","year":"2016"},{"key":"e_1_2_2_7_1","volume-title":"available online. (February","author":"Altenkirch Thorsten","year":"2006"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.46"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"e_1_2_2_14_1","volume-title":"Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR abs\/1611.02108","author":"Cohen Cyril","year":"2016"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_2_2_16_1","first-page":"535","article-title":"Relational limits in general polymorphism","volume":"30","author":"Hasegawa Ryu","year":"1994","journal-title":"Publications of the Research Institute for Mathematical Sciences"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1_2"},{"key":"e_1_2_2_18_1","unstructured":"Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Unpublished note. (1997).  Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Unpublished note. (1997)."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2013.432"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90053-5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_29_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_16"},{"key":"e_1_2_2_32_1","volume-title":"IFIP Congress. 513\u2013523","author":"Reynolds John C.","year":"1983"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316053"},{"key":"e_1_2_2_36_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/ncatlab.org\/homotopytypetheory\/ files\/HTS.pdf unpublished note.  Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/ncatlab.org\/homotopytypetheory\/ files\/HTS.pdf unpublished note."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_38_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\/3110276","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":33,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110276"],"URL":"https:\/\/doi.org\/10.1145\/3110276","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}