{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T05:45:53Z","timestamp":1784180753645,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1553471, 1564207"],"award-info":[{"award-number":["1553471, 1564207"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011030","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0018050"],"award-info":[{"award-number":["DE-SC0018050"]}],"id":[{"id":"10.13039\/100011030","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":[[2018,7,30]]},"abstract":"<jats:p>Abstracting abstract machines is a systematic methodology for constructing sound static analyses for higher-order languages, by deriving small-step abstract abstract machines (AAMs) that perform abstract interpretation from abstract machines that perform concrete evaluation. Darais et al. apply the same underlying idea to monadic definitional interpreters, and obtain monadic abstract definitional interpreters (ADIs) that perform abstract interpretation in big-step style using monads. Yet, the relation between small-step abstract abstract machines and big-step abstract definitional interpreters is not well studied.<\/jats:p>\n          <jats:p>In this paper, we explain their functional correspondence and demonstrate how to systematically transform small-step abstract abstract machines into big-step abstract definitional interpreters. Building on known semantic interderivation techniques from the concrete evaluation setting, the transformations include linearization, lightweight fusion, disentanglement, refunctionalization, and the left inverse of the CPS transform. Linearization expresses nondeterministic choice through first-order data types, after which refunctionalization transforms the first-order data types that represent continuations into higher-order functions. The refunctionalized AAM is an abstract interpreter written in continuation-passing style (CPS) with two layers of continuations, which can be converted back to direct style with delimited control operators. Based on the known correspondence between delimited control and monads, we demonstrate that the explicit use of monads in abstract definitional interpreters is optional.<\/jats:p>\n          <jats:p>All transformations properly handle the collecting semantics and nondeterminism of abstract interpretation. Remarkably, we reveal how precise call\/return matching in control-flow analysis can be obtained by refunctionalizing a small-step abstract abstract machine with proper caching.<\/jats:p>","DOI":"10.1145\/3236800","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)"],"prefix":"10.1145","volume":"2","author":[{"given":"Guannan","family":"Wei","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"Decker","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.02.012"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.008"},{"key":"e_1_2_2_4_1","volume-title":"An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science","author":"Biernacka Malgorzata","year":"2005","unstructured":"Malgorzata Biernacka , Dariusz Biernacki , and Olivier Danvy . 2005. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science Volume 1 , Issue 2 ( Nov. 2005 ). Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 2005. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science Volume 1, Issue 2 (Nov. 2005)."},{"key":"e_1_2_2_5_1","volume-title":"Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language","author":"Biernacka Malgorzata","unstructured":"Malgorzata Biernacka and Olivier Danvy . 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language , Part II: Reduction Semantics and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Jens Palsberg (Ed.), Vol. 5700 . Springer , 186\u2013206. Malgorzata Biernacka and Olivier Danvy. 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Jens Palsberg (Ed.), Vol. 5700. Springer, 186\u2013206."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651902"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154645"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00003-4"},{"key":"e_1_2_2_10_1","volume-title":"CC (Lecture Notes in Computer Science)","author":"Danvy Olivier","unstructured":"Olivier Danvy . 2003. A New One-Pass Transformation into Monadic Normal Form . In CC (Lecture Notes in Computer Science) , Vol. 2622 . Springer , 77\u201389. Olivier Danvy. 2003. A New One-Pass Transformation into Monadic Normal Form. In CC (Lecture Notes in Computer Science), Vol. 2622. Springer, 77\u201389."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11431664_4"},{"key":"e_1_2_2_12_1","volume-title":"An Analytical Approach to Programs as Data Objects. DSc thesis. Department of Computer Science","author":"Danvy Olivier","unstructured":"Olivier Danvy . 2006a. An Analytical Approach to Programs as Data Objects. DSc thesis. Department of Computer Science , Aarhus University , Aarhus, Denmark . Olivier Danvy. 2006a. An Analytical Approach to Programs as Data Objects. DSc thesis. Department of Computer Science, Aarhus University, Aarhus, Denmark."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11783596_2"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411206"},{"key":"e_1_2_2_15_1","volume-title":"Natural Semantics, and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science)","author":"Danvy Olivier","unstructured":"Olivier Danvy . 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics , Natural Semantics, and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science) , Jens Palsberg (Ed.), Vol. 5700 . Springer , 162\u2013185. Olivier Danvy. 2009. Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines. In Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Jens Palsberg (Ed.), Vol. 5700. Springer, 162\u2013185."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_17_1","volume-title":"Representing control: A study of the CPS transformation. Mathematical structures in computer science 2, 4","author":"Danvy Olivier","year":"1992","unstructured":"Olivier Danvy and Andrzej Filinski . 1992. Representing control: A study of the CPS transformation. Mathematical structures in computer science 2, 4 ( 1992 ), 361\u2013391. Olivier Danvy and Andrzej Filinski. 1992. Representing control: A study of the CPS transformation. Mathematical structures in computer science 2, 4 (1992), 361\u2013391."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141564"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.10.010"},{"key":"e_1_2_2_20_1","volume-title":"A Rational Deconstruction of Landin\u2019s SECD Machine with the J Operator. Logical Methods in Computer Science 4, 4","author":"Danvy Olivier","year":"2008","unstructured":"Olivier Danvy and Kevin Millikin . 2008b. A Rational Deconstruction of Landin\u2019s SECD Machine with the J Operator. Logical Methods in Computer Science 4, 4 ( 2008 ). Olivier Danvy and Kevin Millikin. 2008b. A Rational Deconstruction of Landin\u2019s SECD Machine with the J Operator. Logical Methods in Computer Science 4, 4 (2008)."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.10.007"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_2_2_23_1","volume-title":"Nielsen","author":"Danvy Olivier","year":"2004","unstructured":"Olivier Danvy and Lasse R . Nielsen . 2004 . Refocusing in reduction semantics. BRICS Report Series 11, 26 (2004). Olivier Danvy and Lasse R. Nielsen. 2004. Refocusing in reduction semantics. BRICS Report Series 11, 26 (2004)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_2_26_1","volume-title":"Pushdown Control-Flow Analysis of Higher-Order Programs. CoRR abs\/1007.4268","author":"Earl Christopher","year":"2010","unstructured":"Christopher Earl , Matthew Might , and David Van Horn . 2010. Pushdown Control-Flow Analysis of Higher-Order Programs. CoRR abs\/1007.4268 ( 2010 ). arXiv: 1007.4268 http:\/\/arxiv.org\/abs\/1007.4268 Christopher Earl, Matthew Might, and David Van Horn. 2010. Pushdown Control-Flow Analysis of Higher-Order Programs. CoRR abs\/1007.4268 (2010). arXiv: 1007.4268 http:\/\/arxiv.org\/abs\/1007.4268"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364576"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633361"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.2298\/CSIS130923030F"},{"key":"e_1_2_2_33_1","volume-title":"Friedman and Anurag Medhekar","author":"Daniel","year":"2003","unstructured":"Daniel P. Friedman and Anurag Medhekar . 2003 . Tutorial : Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University . Daniel P. Friedman and Anurag Medhekar. 2003. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951936"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661098"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646235.682702"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365257"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806631"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190241"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8611-7"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010075320153"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596596"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54007"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/115865.115884"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000238"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_30"},{"key":"e_1_2_2_54_1","volume-title":"How to replace failure by a list of successes a method for exception handling, backtracking, and pattern matching in lazy functional languages","author":"Wadler Philip","unstructured":"Philip Wadler . 1985. How to replace failure by a list of successes a method for exception handling, backtracking, and pattern matching in lazy functional languages . In Functional Programming Languages and Computer Architecture, Jean-Pierre Jouannaud (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 113\u2013128. Philip Wadler. 1985. How to replace failure by a list of successes a method for exception handling, backtracking, and pattern matching in lazy functional languages. In Functional Programming Languages and Computer Architecture, Jean-Pierre Jouannaud (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113\u2013128."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236800","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236800","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":54,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236800"],"URL":"https:\/\/doi.org\/10.1145\/3236800","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}