Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Mon 4 Sep 2017 16:40 - 17:02 at L1 - Effects Chair(s): Ben Lippmeier

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, \emph{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 \emph{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.

Mon 4 Sep

icfp-2017-papers
16:40 - 18:10: Research Papers - Effects at L1
Chair(s): Ben LippmeierDigital Asset / UNSW Australia
icfp-2017-papers150453600000016:40 - 17:02
Talk
David DaraisUniversity of Maryland, USA, Nicholas LabichUniversity of Maryland, USA, Phúc C. NguyễnUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA
DOI
icfp-2017-papers150453735000017:02 - 17:25
Talk
Yannick ForsterSaarland University, Germany / University of Cambridge, UK, Ohad KammarUniversity of Oxford, UK, Sam LindleyUniversity of Edinburgh, UK, Matija PretnarUniversity of Ljubljana, Slovenia
DOI
icfp-2017-papers150453870000017:25 - 17:47
Talk
Wilmer RicciottiUniversity of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK, Roly PereraUniversity of Edinburgh, UK / University of Glasgow, UK, James CheneyUniversity of Edinburgh, UK
DOI
icfp-2017-papers150454005000017:47 - 18:10
Talk
Jan MidtgaardDTU, Denmark, Mathias Nygaard JustesenDTU, Denmark, Patrick KastingDTU, Denmark, Flemming NielsonDTU, Denmark, Hanne Riis NielsonDTU, Denmark
DOI