Abstracting definitional interpreters (functional pearl)
Open Access
- 29 August 2017
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 1 (ICFP), 1-25
- https://doi.org/10.1145/3110256
Abstract
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. But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, 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 abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called “pushdown control flow” 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. 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.Funding Information
- National Science Foundation (1618756)
This publication has 41 references indexed in Scilit:
- Pushdown control-flow analysis for freePublished by Association for Computing Machinery (ACM) ,2016
- Galois transformers and modular abstract interpreters: reusable metatheory for program analysisPublished by Association for Computing Machinery (ACM) ,2015
- Simulation of Two-Way Pushdown Automata RevisitedElectronic Proceedings in Theoretical Computer Science, 2013
- Introspective pushdown analysis of higher-order programsPublished by Association for Computing Machinery (ACM) ,2012
- Purely functional lazy nondeterministic programmingJournal of Functional Programming, 2011
- A functional correspondence between monadic evaluators and abstract machines for languages with computational effectsTheoretical Computer Science, 2005
- Deriving backtracking monad transformersPublished by Association for Computing Machinery (ACM) ,2000
- UnitsPublished by Association for Computing Machinery (ACM) ,1998
- Practical program analysis using general purpose logic programming systems—a case studyPublished by Association for Computing Machinery (ACM) ,1996
- Tabled evaluation with delaying for general logic programsJournal of the ACM, 1996