{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:34:47Z","timestamp":1770287687631,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"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":["1618756"],"award-info":[{"award-number":["1618756"]}],"id":[{"id":"10.13039\/100000001","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":[[2017,8,29]]},"abstract":"<jats:p>In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a nice basis for a wide variety of collecting semantics, abstract interpretations, symbolic executions, and their intermixings.<\/jats:p>\n          <jats:p>\n            But the real insight of this story is a replaying of an insight from Reynold's landmark paper,\n            <jats:italic>Definitional Interpreters for Higher-Order Programming Languages<\/jats:italic>\n            , in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional\n            <jats:italic>abstract<\/jats:italic>\n            interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called \u201cpushdown control flow\u201d property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language.\n          <\/jats:p>\n          <jats:p>The first approaches to achieve this property for higher-order languages appeared within the last ten years, and have since been the subject of many papers. These approaches start from a state-machine semantics and uniformly involve significant technical engineering to recover the precision of pushdown control flow. In contrast, starting from a definitional interpreter, the pushdown control flow property is inherent in the meta-language and requires no further technical mechanism to achieve.<\/jats:p>","DOI":"10.1145\/3110256","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":46,"title":["Abstracting definitional interpreters (functional pearl)"],"prefix":"10.1145","volume":"1","author":[{"given":"David","family":"Darais","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Nicholas","family":"Labich","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Ph\u00fac C.","family":"Nguyen","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.008"},{"key":"e_1_2_2_2_1","volume-title":"Bol and Lars Degerstedt. Tabulated Resolution for Well Founded Semantics. In Proc. ILPS","author":"Roland","year":"1993","unstructured":"Roland N Bol and Lars Degerstedt. Tabulated Resolution for Well Founded Semantics. In Proc. ILPS , 1993 . Roland N Bol and Lars Degerstedt. Tabulated Resolution for Well Founded Semantics. In Proc. ILPS, 1993."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227597"},{"key":"e_1_2_2_4_1","volume-title":"Proc. Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications","author":"Darais David","year":"2015","unstructured":"David Darais , Matthew Might , and David Van Horn . Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis . In Proc. Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 2015 . David Darais, Matthew Might, and David Van Horn. Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis. In Proc. Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231399"},{"key":"e_1_2_2_7_1","volume-title":"Proc. Workshop on Scheme and Functional Programming","author":"Earl Christopher","year":"2010","unstructured":"Christopher Earl , Matthew Might , and David Van Horn . Pushdown control-flow analysis of higher-order programs . In Proc. Workshop on Scheme and Functional Programming , 2010 . Christopher Earl, Matthew Might, and David Van Horn. Pushdown control-flow analysis of higher-order programs. In Proc. Workshop on Scheme and Functional Programming, 2010."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364576"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000189"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277730"},{"key":"e_1_2_2_11_1","volume-title":"Racket","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. Reference : Racket . PLT Inc ., 2010 . Matthew Flatt and PLT. Reference: Racket. PLT Inc., 2010."},{"key":"e_1_2_2_12_1","volume-title":"Course notes for CSCI B621","author":"Daniel","year":"2003","unstructured":"Daniel P. Friedman and Anurag Medhekar. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation , Course notes for CSCI B621 , Indiana University . 2003 . Daniel P. Friedman and Anurag Medhekar. Tutorial: Using an Abstracted Interpreter to Understand Abstract Interpretation, Course notes for CSCI B621, Indiana University. 2003."},{"key":"e_1_2_2_13_1","volume-title":"David Van Horn. Pushdown Controlflow Analysis for Free. In Proc. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Gilray Thomas","year":"2016","unstructured":"Thomas Gilray , Steven Lyde , Michael D. Adams , Matthew Might , and David Van Horn. Pushdown Controlflow Analysis for Free. In Proc. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , 2016 . Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. Pushdown Controlflow Analysis for Free. In Proc. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.129.15"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351258"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268973"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199536"},{"key":"e_1_2_2_18_1","volume-title":"Janssens and Konstantinos F Sagonas. On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems. In Proc. TAPD","author":"Gerda","year":"1998","unstructured":"Gerda Janssens and Konstantinos F Sagonas. On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems. In Proc. TAPD , 1998 . Gerda Janssens and Konstantinos F Sagonas. On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems. In Proc. TAPD, 1998."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000100"},{"key":"e_1_2_2_21_1","volume-title":"Johnson and David Van Horn. Abstracting Abstract Control. In Proc. Proceedings of the 10th ACM Symposium on Dynamic Languages","author":"Ian J.","year":"2014","unstructured":"J. Ian Johnson and David Van Horn. Abstracting Abstract Control. In Proc. Proceedings of the 10th ACM Symposium on Dynamic Languages , 2014 . J. Ian Johnson and David Van Horn. Abstracting Abstract Control. In Proc. Proceedings of the 10th ACM Symposium on Dynamic Languages, 2014."},{"key":"e_1_2_2_22_1","series-title":"Vol. 4","volume-title":"Proc. Handbook of Logic in Computer Science","author":"Neil","year":"1995","unstructured":"Neil D. Jones and Flemming Nielson. Abstract Interpretation: A Semantics-based Tool for Program Analysis . In Proc. Handbook of Logic in Computer Science ( Vol. 4 ) , 1995 . Neil D. Jones and Flemming Nielson. Abstract Interpretation: A Semantics-based Tool for Program Analysis. In Proc. Handbook of Logic in Computer Science (Vol. 4), 1995."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32202-0_3"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086390"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187672"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_23"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596592"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190247"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111049"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159807"},{"key":"e_1_2_2_34_1","volume-title":"Might and David Van Horn. A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-OrderPrograms. In Proc. Static Analysis","author":"Matthew","year":"2011","unstructured":"Matthew Might and David Van Horn. A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-OrderPrograms. In Proc. Static Analysis , 2011 . Matthew Might and David Van Horn. A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-OrderPrograms. In Proc. Static Analysis, 2011."},{"key":"e_1_2_2_35_1","volume-title":"An Abstract View of Programming Languages","author":"Moggi Eugenio","year":"1989","unstructured":"Eugenio Moggi . An Abstract View of Programming Languages . Edinburgh University , 1989 . Eugenio Moggi. An Abstract View of Programming Languages. Edinburgh University, 1989."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224182"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","year":"1999","unstructured":"Flemming Nielson , Hanne R. Nielson , and Chris Hankin . Principles of Program Analysis . 1999 . Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. 1999."},{"key":"e_1_2_2_40_1","volume-title":"Proc. Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell","author":"van der Ploeg Atze","year":"2014","unstructured":"Atze van der Ploeg and Oleg Kiselyov . Reflection without remorse: revealing a hidden sequence to speed up monadic reflection . In Proc. Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell , 2014 . Atze van der Ploeg and Oleg Kiselyov. Reflection without remorse: revealing a hidden sequence to speed up monadic reflection. In Proc. Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, 2014."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000500"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16492-8_66"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993514"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000238"},{"key":"e_1_2_2_51_1","volume-title":"Proc. IFL 2015: Symposium on the implementation and application of functional programming languages Proceedings","author":"Vandenbroucke Alexander","year":"2016","unstructured":"Alexander Vandenbroucke , Tom Schrijvers , and Frank Piessens . Fixing non-determinism . In Proc. IFL 2015: Symposium on the implementation and application of functional programming languages Proceedings , 2016 . Alexander Vandenbroucke, Tom Schrijvers, and Frank Piessens. Fixing non-determinism. In Proc. IFL 2015: Symposium on the implementation and application of functional programming languages Proceedings, 2016."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:3)2011"},{"key":"e_1_2_2_54_1","volume-title":"ACM Trans. Program. Lang. Syst.","author":"Andrew","year":"1998","unstructured":"Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis . ACM Trans. Program. Lang. Syst. , 1998 . Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 1998."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110256","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110256","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110256"],"URL":"https:\/\/doi.org\/10.1145\/3110256","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}