{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:53Z","timestamp":1750220393399,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["TH 665\/11-1"],"award-info":[{"award-number":["TH 665\/11-1"]}],"id":[{"id":"10.13039\/501100001659","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,10,20]]},"abstract":"<jats:p>Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a means to vary the level of typing precision between program fragments and to transition smoothly towards more precisely typed programs. The combination of gradual typing and dependent types seems promising to promote the widespread use of dependent types.<\/jats:p>\n          <jats:p>We investigate a gradual version of a minimalist value-dependent lambda calculus. Compile-time calculations and thus dependencies are restricted to labels, drawn from a generic enumeration type. The calculus supports the usual Pi and Sigma types as well as singleton types and subtyping. It is sufficiently powerful to provide flexible encodings of variant and record types with first-class labels.<\/jats:p>\n          <jats:p>We provide type checking algorithms for the underlying label-dependent lambda calculus and its gradual extension. The gradual type checker drives the translation into a cast calculus, which extends the original language. The cast calculus comes with several innovations: refined typing for casts in the presence of singletons, type reduction in casts, and fully dependent Sigma types. Besides standard metatheoretical results, we establish the gradual guarantee for the gradual language.<\/jats:p>","DOI":"10.1145\/3485485","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Label dependent lambda calculus and gradual typing"],"prefix":"10.1145","volume":"5","author":[{"given":"Weili","family":"Fu","sequence":"first","affiliation":[{"name":"University of Freiburg, Germany"}]},{"given":"Fabian","family":"Krause","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9000-1239","authenticated-orcid":false,"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_10"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00175-4"},{"volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","key":"e_1_2_2_4_1"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"volume-title":"Siek","year":"2016","author":"Cimini Matteo","key":"e_1_2_2_8_1"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.291.5"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. In POPL. ACM 429\u2013442.  Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. In POPL. ACM 429\u2013442.","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110282"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5497628"},{"volume-title":"POPL","author":"Lehmann Nico","key":"e_1_2_2_20_1"},{"volume-title":"Gradualizing the Calculus of Inductive Constructions. CoRR, abs\/2011.10618","year":"2020","author":"Lennon-Bertrand Meven","key":"e_1_2_2_21_1"},{"key":"e_1_2_2_22_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli.  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:7)2020"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268968"},{"key":"e_1_2_2_26_1","first-page":"04651","volume-title":"Doaitse Swierstra (Eds.) (LNCS","volume":"266","author":"Norell Ulf","year":"2008"},{"volume-title":"Dynamic Typing with Dependent Types","author":"Ou Xinming","key":"e_1_2_2_27_1"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop.","author":"Jeremy","key":"e_1_2_2_32_1"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_2_2_34_1","volume-title":"SNAPL (LIPIcs","volume":"293","author":"Siek Jeremy G.","year":"2015"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.76.9"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000142"},{"volume-title":"Bierman","year":"2014","author":"Swamy Nikhil","key":"e_1_2_2_40_1"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816710"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_2_44_1","unstructured":"2021. TypeScript Handbook Advanced Types. https:\/\/www.typescriptlang.org\/docs\/handbook\/advanced-types.html  2021. TypeScript Handbook Advanced Types. https:\/\/www.typescriptlang.org\/docs\/handbook\/advanced-types.html"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341705"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485485","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485485","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:39Z","timestamp":1750191519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485485"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":46,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485485"],"URL":"https:\/\/doi.org\/10.1145\/3485485","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}