{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:21Z","timestamp":1781855601829,"version":"3.54.5"},"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 toggle=\"yes\">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 toggle=\"yes\">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 toggle=\"yes\">nameless<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">co-contextual<\/jats:italic>\n                    representation of typed global label binding, which\n                    <jats:italic toggle=\"yes\">is<\/jats:italic>\n                    compositional. Our key idea is to use\n                    <jats:italic toggle=\"yes\">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-04T12:34:24Z","timestamp":1609763664000},"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":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands \/ Delft University of Technology, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eelco","family":"Visser","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","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."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch James Chapman and Tarmo Uustalu. 2015. Monads need not be endofunctors. Logical Methods in Computer Science (LMCS) 11 1 ( 2015 ). https:\/\/doi.org\/10.2168\/LMCS-11 ( 1 :3) 2015 10.2168\/LMCS-11(1:3)2015","DOI":"10.2168\/LMCS-11"},{"key":"e_1_2_1_3_1","volume-title":"Formal Techniques for Java-like Programs Workshop (FTfJP).","author":"Ancona Davide","year":"2004","unstructured":"Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca, et al. 2004. Even more principal typings for Java-like languages. In Formal Techniques for Java-like Programs Workshop (FTfJP)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_1_8_1","volume-title":"Workshop on Dependent Types in Programming.","author":"Augustsson Lennart","year":"1999","unstructured":"Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. In Workshop on Dependent Types in Programming."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27694-1_18"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604149"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814277"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237728"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming (JFP) 28 ( 2018 ) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146811"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Anders Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik 23 1 ( 1972 ) 113-120.","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.18"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 7 ( 2009 ) 107-115. https:\/\/doi.org\/10.1145\/ 1538788.1538814 10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_28_1","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."},{"key":"e_1_2_1_29_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).","DOI":"10.1145\/2364527.2364529"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.275.6"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"e_1_2_1_32_1","unstructured":"James McKinna and Joel Wright. 2006. A type-correct stack-safe provably correct expression compiler. Unpublished draft."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93 1 ( 1991 ) 55-92. https: \/\/doi.org\/10.1016\/ 0890-5401 ( 91 ) 90052-4 10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_35_1","volume-title":"Workshop on Compiler Support for System Software. 25-35","author":"Morrisett Greg","year":"1999","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. 1999a. TALx86: A realistic typed assembly language. In Workshop on Compiler Support for System Software. 25-35."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0_7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236965"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"John C Reynolds. 2000. The meaning of types from intrinsic to extrinsic semantics. BRICS Report Series 7 32 ( 2000 ).","DOI":"10.7146\/brics.v7i32.20167"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Arjen Rouvoet Robbert Krebbers and Eelco Visser. 2020b. Intrinsically Typed Compilation with Nameless labels: Agda Sources. https:\/\/doi.org\/10.5281\/zenodo.4072068 10.5281\/zenodo.4072068","DOI":"10.5281\/zenodo.4072068"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Arjen Rouvoet Robbert Krebbers and Eelco Visser. 2020c. Intrinsically Typed Compilation with Nameless labels: Virtual Machine. https:\/\/doi.org\/10.5281\/zenodo.4071954 10.5281\/zenodo.4071954","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","unstructured":"David Walker. 2005. Substructural type systems. In Advanced topics in types and programming languages, Benjamin C Pierce (Ed.). The MIT press, Chapter 1, 3-43.","journal-title":"Chapter"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","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":[[2026,6,19]],"date-time":"2026-06-19T07:28:35Z","timestamp":1781854115000},"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":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}