{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:12:19Z","timestamp":1770289939998,"version":"3.49.0"},"reference-count":55,"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\/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>Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.<\/jats:p>\n          <jats:p>\n            In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier \u2200 which lets us ignore sizes in terms for equality checking, alongside with a second quantifier \u03a0 for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features\n            <jats:italic>type shape<\/jats:italic>\n            -directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.\n          <\/jats:p>","DOI":"10.1145\/3110277","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Normalization by evaluation for sized dependent types"],"prefix":"10.1145","volume":"1","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[{"name":"University of Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Theo","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"ENS Paris-Saclay, France"}],"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.2168\/LMCS-4(2:3)2008"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_17"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.1"},{"key":"e_1_2_2_4_1","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Unpublished. http:\/\/www.tcs.ifi. lmu.de\/~abel\/habil.pdf  Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Unpublished. http:\/\/www.tcs.ifi. lmu.de\/~abel\/habil.pdf"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004191"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_3"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:4)2011"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_2_2_11_1","unstructured":"AgdaTeam. 2017. The Agda Wiki. (2017). http:\/\/wiki.portal.chalmers.se\/agda  AgdaTeam. 2017. The Agda Wiki. (2017). http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053541"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_18"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_2"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_11"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_8"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.084"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47018-2_16"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_12"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_2"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_24"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789814368452_0004"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_40_1","unstructured":"INRIA. 2016. The Coq Proof Assistant Reference Manual (version 8.6 ed.). INRIA. http:\/\/coq.inria.fr\/  INRIA. 2016. The Coq Proof Assistant Reference Manual (version 8.6 ed.). INRIA. http:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_15"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:5)2010"},{"key":"e_1_2_2_44_1","volume-title":"Logic Colloquium \u201873","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f . 1975. An Intuitionistic Theory of Types: Predicative Part . In Logic Colloquium \u201873 , H. E. Rose and J. C. Shepherdson (Eds.). North-Holland , 73\u2013118. Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium \u201873, H. E. Rose and J. C. Shepherdson (Eds.). North-Holland, 73\u2013118."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855752"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941137"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.29"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_11"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.6"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_56_1","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"Werner Benjamin","year":"1992","unstructured":"Benjamin Werner . 1992 . A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers . In Proceedings of the 1992 Workshop on Types for Proofs and Programs , B\u00e5stad, Sweden , June 1992, Bengt Nordstr\u00f6m, Kent Petersson, and Gordon Plotkin (Eds.). 341\u2013357. http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/Types\/proc92.ps Benjamin Werner. 1992. A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, June 1992, Bengt Nordstr\u00f6m, Kent Petersson, and Gordon Plotkin (Eds.). 341\u2013357. http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/Types\/proc92.ps"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110277","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110277","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\/3110277"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":55,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110277"],"URL":"https:\/\/doi.org\/10.1145\/3110277","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"}}]}}