{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:10:14Z","timestamp":1770282614112,"version":"3.49.0"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NWO","award":["639.023.206"],"award-info":[{"award-number":["639.023.206"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects?<\/jats:p>\n          <jats:p>\n            In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed \u03bb-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A\n            <jats:italic>dependent-passing style<\/jats:italic>\n            technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with\n            <jats:italic>scope graphs<\/jats:italic>\n            and\n            <jats:italic>frames<\/jats:italic>\n            , which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed \u03bb-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ).\n          <\/jats:p>","DOI":"10.1145\/3158104","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Intrinsically-typed definitional interpreters for imperative languages"],"prefix":"10.1145","volume":"2","author":[{"given":"Casper","family":"Bach Poulsen","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arjen","family":"Rouvoet","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Tolmach","sequence":"additional","affiliation":[{"name":"Portland State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"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":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4317"},{"key":"e_1_2_2_2_1","volume-title":"Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2018","author":"Ahman Danel","year":"2018","unstructured":"Danel Ahman , C\u00e9dric Fournet , Catalin Hritcu , Kenji Maillard , Aseem Rastogi , and Nikhil Swamy . 2018 . Recalling a Witness . In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2018 , Los Angeles, CA, USA , January 8-13, 2018 . ACM. Danel Ahman, C\u00e9dric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. 2018. Recalling a Witness. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2018, Los Angeles, CA, USA, January 8-13, 2018 . ACM."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_2_2_10_1","volume-title":"In Workshop on Dependent Types in Programming, Gothenburg .","author":"Augustsson Lennart","year":"1999","unstructured":"Lennart Augustsson and Magnus Carlsson . 1999 . An exercise in dependent types: A well-typed interpreter . In In Workshop on Dependent Types in Programming, Gothenburg . Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. In In Workshop on Dependent Types in Programming, Gothenburg ."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.20"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Casper Bach Poulsen Arjen Rouvoet Andrew Tolmach Robbert Krebbers and Eelco Visser. 2017. Artifact Intrinsically-Typed Definitional Interpreters for Imperative Languages. https:\/\/github.com\/metaborg\/mj.agda  Casper Bach Poulsen Arjen Rouvoet Andrew Tolmach Robbert Krebbers and Eelco Visser. 2017. Artifact Intrinsically-Typed Definitional Interpreters for Imperative Languages. https:\/\/github.com\/metaborg\/mj.agda","DOI":"10.1145\/3158104"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4650"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_16_1","volume-title":"MJ: An imperative core calculus for Java and Java with effects. Technical Report UCAM-CL-TR-563","author":"Bierman G. M.","year":"2003","unstructured":"G. M. Bierman , M. J. Parkinson , and A. M. Pitts . 2003 . MJ: An imperative core calculus for Java and Java with effects. Technical Report UCAM-CL-TR-563 . University of Cambridge . G. M. Bierman, M. J. Parkinson, and A. M. Pitts. 2003. MJ: An imperative core calculus for Java and Java with effects. Technical Report UCAM-CL-TR-563. University of Cambridge."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173724"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_2_2_24_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant . MIT Press . Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_2_2_26_1","volume-title":"Siek","author":"Cimini Matteo","year":"2016","unstructured":"Matteo Cimini , Dale Miller , and Jeremy G . Siek . 2016 . Well-Typed Languages are Sound. CoRR abs\/1611.05105 (2016). http:\/\/arxiv.org\/abs\/1611.05105 Matteo Cimini, Dale Miller, and Jeremy G. Siek. 2016. Well-Typed Languages are Sound. CoRR abs\/1611.05105 (2016). http:\/\/arxiv.org\/abs\/1611.05105"},{"key":"e_1_2_2_27_1","volume-title":"Lecture Notes in Computer Science","volume":"4350","author":"Clavel Manuel","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn L . Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic . Lecture Notes in Computer Science , Vol. 4350 . Springer. Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic . Lecture Notes in Computer Science, Vol. 4350. Springer."},{"key":"e_1_2_2_28_1","unstructured":"The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr\/doc\/  The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr\/doc\/"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364546"},{"key":"e_1_2_2_30_1","unstructured":"Nils Anders Danielsson and U Norell. 2017. The Agda standard library. https:\/\/github.com\/agda\/agda-stdlib  Nils Anders Danielsson and U Norell. 2017. The Agda standard library. https:\/\/github.com\/agda\/agda-stdlib"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048113"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814228.2814239"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_2_2_37_1","volume-title":"Stone","author":"Harper Robert","year":"2000","unstructured":"Robert Harper and Christopher A . Stone . 2000 . A type-theoretic interpretation of standard ML. In Proof, Language, and Interaction, Essays in Honour of Robin Milner , Gordon D. Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press , 341\u2013388. Robert Harper and Christopher A. Stone. 2000. A type-theoretic interpretation of standard ML. In Proof, Language, and Interaction, Essays in Honour of Robin Milner , Gordon D. Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press, 341\u2013388."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869497"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103691"},{"key":"e_1_2_2_41_1","volume-title":"Jinja is not Java. Archive of Formal Proofs 2005","author":"Klein Gerwin","year":"2005","unstructured":"Gerwin Klein and Tobias Nipkow . 2005. Jinja is not Java. Archive of Formal Proofs 2005 ( 2005 ). Gerwin Klein and Tobias Nipkow. 2005. Jinja is not Java. Archive of Formal Proofs 2005 (2005)."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146811"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36089-3_18"},{"key":"e_1_2_2_45_1","volume-title":"Licata","author":"Korkut Joomy","year":"2016","unstructured":"Joomy Korkut , Maksim Trifunovski , and Daniel R . Licata . 2016 . Intrinsic Verification of a Regular Expression Matcher . (2016). http:\/\/dlicata.web.wesleyan.edu\/pubs\/ktl16regexp\/ktl16regexp.pdf Unpublished draft. Joomy Korkut, Maksim Trifunovski, and Daniel R. Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. (2016). http:\/\/dlicata.web.wesleyan.edu\/pubs\/ktl16regexp\/ktl16regexp.pdf Unpublished draft."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481851"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837644"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2318202.2318206"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_2_2_51_1","unstructured":"Conor McBride. 2011. Kleisli Arrows of Outrageous Fortune. (2011). Accepted for publication.  Conor McBride. 2011. Kleisli Arrows of Outrageous Fortune. (2011). Accepted for publication."},{"key":"e_1_2_2_52_1","volume-title":"Revised","author":"Milner Robin","unstructured":"Robin Milner , Mads Tofte , Robert Harper , and David MacQueen . 1997. The Definition of Standard ML , Revised . MIT Press , Cambridge, MA, USA . Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML, Revised. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_54_1","volume-title":"A Modular SOS for ML Concurrency Primitives. BRICS Research Series RS-99-57. Department of Computer Science","author":"Mosses Peter D.","unstructured":"Peter D. Mosses . 1999. A Modular SOS for ML Concurrency Primitives. BRICS Research Series RS-99-57. Department of Computer Science , Aarhus University . Peter D. Mosses. 1999. A Modular SOS for ML Concurrency Primitives. BRICS Research Series RS-99-57. Department of Computer Science, Aarhus University."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_9"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_2_62_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages . MIT Press, Cambridge , Massachusetts . Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, Massachusetts."},{"key":"e_1_2_2_63_1","unstructured":"The Racket Development Team. 2017. Racket v6.11. http:\/\/blog.racket-lang.org\/2017\/10\/racket-v6-11.html  The Racket Development Team. 2017. Racket v6.11. http:\/\/blog.racket-lang.org\/2017\/10\/racket-v6-11.html"},{"key":"e_1_2_2_64_1","volume-title":"The Meaning of Types \u2013 From Intrinsic to Extrinsic Semantics. BRICS Research Series RS-00-32. Department of Computer Science","author":"Reynolds John","unstructured":"John Reynolds . 2004. The Meaning of Types \u2013 From Intrinsic to Extrinsic Semantics. BRICS Research Series RS-00-32. Department of Computer Science , Aarhus University . John Reynolds. 2004. The Meaning of Types \u2013 From Intrinsic to Extrinsic Semantics. BRICS Research Series RS-00-32. Department of Computer Science, Aarhus University."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_2_67_1","unstructured":"Jeremy G. Siek. 2013. Type Safety in Three Easy Lemmas. http:\/\/siek.blogspot.co.uk\/2013\/05\/ type-safety-in-three-easy-lemmas.html .  Jeremy G. Siek. 2013. Type Safety in Three Easy Lemmas. http:\/\/siek.blogspot.co.uk\/2013\/05\/ type-safety-in-three-easy-lemmas.html ."},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064899.3064906"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2847538.2847543"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892664.2893464"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2015.365"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661136.2661149"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158104","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":76,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158104"],"URL":"https:\/\/doi.org\/10.1145\/3158104","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}