ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Mon 13 Oct 2025 13:40 - 14:05 at Orchid Plenary Ballroom - Distinguished Papers Chair(s): Dominique Devriese

Over the last 15 years, several popular systematic abstraction frameworks have emerged—frameworks that allow a static analysis to be derived by systematically transforming a concrete semantics. These frameworks guarantee computability of the resulting artifact by the application of an a priori abstraction which induces a particular finitization in the execution space. While effective, this abstraction occurs without regard for program structure, subjecting each program point to the same fixed degree of context sensitivity. In this paper, we present CGADI, an enhancement to systematic abstraction frameworks based on definitional interpreters which defers abstraction until a parameterized safety property signals that it should be applied. We then examine this enhanced framework instantiated with two such safety properties: a simple reentrancy property which detects non-recursive portions of program execution, and a size change property which detects evaluation paths destined to converge by virtue of appropriately decreasing values along them. The result is that CGADI can operate in the fully-precise concrete space for portions of execution without forfeiting computability. Our evaluation demonstrates that CGADI is able to produce a higher number of precise results than a corresponding CFA at relatively low cost and that, with no special treatment, CGADI can handle many programming patterns targeted by specific analysis techniques.

Mon 13 Oct

Displayed time zone: Perth change

13:40 - 15:20
Distinguished PapersICFP Papers at Orchid Plenary Ballroom
Chair(s): Dominique Devriese KU Leuven
13:40
25m
Talk
Call-Guarded Abstract Definitional InterpretersDistinguished Paper
ICFP Papers
Kimball Germane Brigham Young University
DOI
14:05
25m
Talk
Effectful Lenses: There and Back with Different MonadsDistinguished Paper
ICFP Papers
Ruifeng Xie Peking University, Tom Schrijvers KU Leuven, Zhenjiang Hu Peking University
DOI
14:30
25m
Talk
First-Order LazinessDistinguished Paper
ICFP Papers
Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh
DOI Pre-print
14:55
25m
Talk
Multi-stage Programming with Splice VariablesDistinguished Paper
ICFP Papers
Tsung-Ju Chiang University of Toronto, Ningning Xie University of Toronto
DOI