{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:23Z","timestamp":1767929543587,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr&aring;det","doi-asserted-by":"publisher","award":["2019-04216"],"award-info":[{"award-number":["2019-04216"]}],"id":[{"id":"10.13039\/501100004359","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":[[2023,8,30]]},"abstract":"<jats:p>\n            We present a graded modal type theory, a dependent type theory with\n            <jats:italic>grades<\/jats:italic>\n            that can be used to enforce various properties of the  \ncode.  \nThe theory has \u03a0-types, weak and strong \u03a3-types, natural numbers, an  \nempty type, and a universe, and we also extend the theory with a unit  \ntype and graded \u03a3-types.  \nThe theory is parameterized by a modality, a kind of partially ordered  \nsemiring, whose elements (grades) are used to track the usage of  \nvariables in terms and types.  \nDifferent modalities are possible.  \nWe focus mainly on quantitative properties, in particular erasure:  \nwith the erasure modality one can mark function arguments as erasable.\n          <\/jats:p>\n          <jats:p>\n            The theory is fully formalized in Agda.  \nThe formalization, which uses a syntactic Kripke logical relation at  \nits core and is based on earlier work, establishes major  \nmeta-theoretic properties such as subject reduction, consistency,  \nnormalization, and decidability of definitional equality.  \nWe also prove a substitution theorem for grade assignment, and  \npreservation of grades under reduction.  \nFurthermore we study an extraction function that translates terms to  \nan untyped \u03bb-calculus and removes erasable content, in  \nparticular function arguments with the \u201cerasable\u201d grade.  \nFor a certain class of modalities we prove that extraction is sound,  \nin the sense that programs of natural number type have the same value  \nbefore and after extraction.  \nSoundness of extraction holds also for\n            <jats:italic>open<\/jats:italic>\n            programs, as  \nlong as all variables in the context are erasable, the context is  \nconsistent, and\n            <jats:italic>erased matches<\/jats:italic>\n            are not allowed for weak  \n\u03a3-types.\n          <\/jats:p>","DOI":"10.1145\/3607862","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"920-954","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0420-4492","authenticated-orcid":false,"given":"Andreas","family":"Abel","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Sweden \/ University of Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8688-0333","authenticated-orcid":false,"given":"Nils Anders","family":"Danielsson","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden \/ University of Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9505-4545","authenticated-orcid":false,"given":"Oskar","family":"Eriksson","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden \/ University of Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11753728_39"},{"key":"e_1_2_1_2_1","volume-title":"Resourceful Dependent Types. In 24th International Conference on Types for Proofs and Programs, TYPES 2018","author":"Abel Andreas","year":"2018","unstructured":"Andreas Abel. 2018. Resourceful Dependent Types. In 24th International Conference on Types for Proofs and Programs, TYPES 2018, Abstracts. 7\u20138. https:\/\/types2018.projj.eu\/book-of-abstracts\/"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_4_1","volume-title":"On the Decidability of Conversion in Type Theory. In TYPES 2016, Types for Proofs and Programs, 22nd Meeting, Book of Abstracts. 5\u20136. http:\/\/www.types2016","author":"Abel Andreas","year":"2016","unstructured":"Andreas Abel, Thierry Coquand, and Bassel Mannaa. 2016. On the Decidability of Conversion in Type Theory. In TYPES 2016, Types for Proofs and Programs, 22nd Meeting, Book of Abstracts. 5\u20136. http:\/\/www.types2016.uns.ac.rs\/images\/abstracts\/abel1.pdf"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8119348"},{"key":"e_1_2_1_6_1","volume-title":"Nils Anders Danielsson, and Andrea Vezzosi","author":"Abel Andreas","year":"2021","unstructured":"Andreas Abel, Nils Anders Danielsson, and Andrea Vezzosi. 2021. Compiling Programs with Erased Univalence. Draft. https:\/\/www.cse.chalmers.se\/~nad\/publications\/abel-danielsson-vezzosi-erased-univalence.html"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_15"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004282"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:28)2022"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:2)2020"},{"key":"e_1_2_1_30_1","unstructured":"Martin Steffen. 1998. Polarized Higher-Order Subtyping. Ph. D. Dissertation. Universit\u00e4t Erlangen-N\u00fcrnberg."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473574"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408973"},{"issue":"6","key":"e_1_2_1_33_1","first-page":"3","article-title":"Agda User Manual","volume":"2","author":"Team The Agda","year":"2023","unstructured":"The Agda Team. 2023. Agda User Manual, Release 2.6.3. https:\/\/readthedocs.org\/projects\/agda\/downloads\/pdf\/v2.6.3\/","journal-title":"Release"},{"key":"e_1_2_1_34_1","first-page":"17","article-title":"The Coq Reference Manual","volume":"8","author":"Development Team The Coq","year":"2023","unstructured":"The Coq Development Team. 2023. The Coq Reference Manual, Release 8.17.1. https:\/\/github.com\/coq\/coq\/releases\/download\/V8.17.1\/coq-8.17.1-reference-manual.pdf","journal-title":"Release"},{"key":"e_1_2_1_35_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics (first ed.). https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.353.10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607862","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607862"],"URL":"https:\/\/doi.org\/10.1145\/3607862","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}