{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:57Z","timestamp":1750220517190,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"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":[[2021,1,4]]},"abstract":"<jats:p>\n            To avoid compilation errors it is desirable to verify that a compiler is\n            <jats:italic>type correct<\/jats:italic>\n            \u2014i.e., given well-typed source code, it always outputs well-typed target code. This can be done\n            <jats:italic>intrinsically<\/jats:italic>\n            by implementing it as a function in a dependently typed programming language, such as Agda. This function manipulates data types of well-typed source and target programs, and is therefore type correct by construction. A key challenge in implementing an intrinsically typed compiler is the representation of labels in bytecode. Because label names are global, bytecode typing appears to be inherently a non-compositional, whole-program property. The individual operations of the compiler do not preserve this property, which requires the programmer to reason about labels, which spoils the compiler definition with proof terms.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we address this problem using a new\n            <jats:italic>nameless<\/jats:italic>\n            and\n            <jats:italic>co-contextual<\/jats:italic>\n            representation of typed global label binding, which\n            <jats:italic>is<\/jats:italic>\n            compositional. Our key idea is to use\n            <jats:italic>linearity<\/jats:italic>\n            to ensure that all labels are defined exactly once. To write concise compilers that manipulate programs in our representation, we develop a linear, dependently typed, shallowly embedded language in Agda, based on separation logic. We show that this language enables the concise specification and implementation of intrinsically typed operations on bytecode, culminating in an intrinsically typed compiler for a language with structured control-flow.\n          <\/jats:p>","DOI":"10.1145\/3434303","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Intrinsically typed compilation with nameless labels"],"prefix":"10.1145","volume":"5","author":[{"given":"Arjen","family":"Rouvoet","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands \/ Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eelco","family":"Visser","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"unstructured":"Andreas Abel. 2020. Type-preserving compilation via dependently typed syntax in Agda. Abstract of a talk at TYPES available online at http:\/\/www.cse.chalmers.se\/~abela\/types20.pdf slides available online at http:\/\/www.cse.chalmers.se\/ ~abela\/talkTYPES2020.pdf.  Andreas Abel. 2020. Type-preserving compilation via dependently typed syntax in Agda. Abstract of a talk at TYPES available online at http:\/\/www.cse.chalmers.se\/~abela\/types20.pdf slides available online at http:\/\/www.cse.chalmers.se\/ ~abela\/talkTYPES2020.pdf.","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.2168\/LMCS-11(1:3)2015"},{"volume-title":"Formal Techniques for Java-like Programs Workshop (FTfJP).","year":"2004","author":"Ancona Davide","key":"e_1_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1109\/LICS.2001.932501"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1017\/CBO9780511609619"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1017\/S095679680900728X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/3209108.3209189"},{"volume-title":"Workshop on Dependent Types in Programming.","year":"1999","author":"Augustsson Lennart","key":"e_1_2_1_8_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.6092\/issn.1972-5787\/5122"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/s10817-011-9219-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/3158093"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1017\/S095679681300018X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-642-27694-1_18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1109\/LICS.2007.30"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/1250734.1250742"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.4230\/LIPIcs.TYPES.2019.2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/640128.604149"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1007\/978-3-642-10672-9_13"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/2814270.2814277"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/1411204.1411218"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/237721.237728"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1017\/S0956796818000151"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/1146811"},{"doi-asserted-by":"crossref","unstructured":"Anders Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik 23 1 ( 1972 ) 113-120.  Anders Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik 23 1 ( 1972 ) 113-120.","key":"e_1_2_1_24_1","DOI":"10.1007\/BF01304852"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.4230\/LIPIcs.ECOOP.2017.18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/2535838.2535841"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/1538788.1538814"},{"unstructured":"Tim Lindholm Frank Yellin Gilad Bracha Alex Buckley and Daniel Smith. 2020. The Java Virtual Machine specification: Java SE 14 edition. Available online at https:\/\/docs.oracle.com\/javase\/specs\/jvms\/se14\/jvms14.pdf.  Tim Lindholm Frank Yellin Gilad Bracha Alex Buckley and Daniel Smith. 2020. The Java Virtual Machine specification: Java SE 14 edition. Available online at https:\/\/docs.oracle.com\/javase\/specs\/jvms\/se14\/jvms14.pdf.","key":"e_1_2_1_28_1"},{"doi-asserted-by":"crossref","unstructured":"Conor McBride. 2012. Agda-curious? https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2364527.2364529 Keynote at the ACM SIGPLAN International Conference of Functional Programming (ICFP).  Conor McBride. 2012. Agda-curious? https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2364527.2364529 Keynote at the ACM SIGPLAN International Conference of Functional Programming (ICFP).","key":"e_1_2_1_29_1","DOI":"10.1145\/2364527.2364529"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.4204\/EPTCS.275.6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1145\/2628136.2628163"},{"unstructured":"James McKinna and Joel Wright. 2006. A type-correct stack-safe provably correct expression compiler. Unpublished draft.  James McKinna and Joel Wright. 2006. A type-correct stack-safe provably correct expression compiler. Unpublished draft.","key":"e_1_2_1_32_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1016\/0022-0000(78)90014-4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1016\/0890-5401(91)90052-4"},{"volume-title":"Workshop on Compiler Support for System Software. 25-35","year":"1999","author":"Morrisett Greg","key":"e_1_2_1_35_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/319301.319345"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/978-3-319-10542-0_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1145\/1481861.1481862"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.2307\/421090"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1145\/3341714"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1145\/3236950.3236965"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1145\/3158104"},{"doi-asserted-by":"crossref","unstructured":"John C Reynolds. 2000. The meaning of types from intrinsic to extrinsic semantics. BRICS Report Series 7 32 ( 2000 ).  John C Reynolds. 2000. The meaning of types from intrinsic to extrinsic semantics. BRICS Report Series 7 32 ( 2000 ).","key":"e_1_2_1_43_1","DOI":"10.7146\/brics.v7i32.20167"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1145\/3372885.3373818"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.5281\/zenodo.4072068"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.5281\/zenodo.4071954"},{"key":"e_1_2_1_47_1","first-page":"3","article-title":"Substructural type systems. In Advanced topics in types and programming languages, Benjamin C Pierce (Ed.). The MIT press","volume":"1","author":"Walker David","year":"2005","journal-title":"Chapter"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1007\/3-540-45465-9_78"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434303"],"URL":"https:\/\/doi.org\/10.1145\/3434303","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}