ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Tue 5 Sep 2023 15:00 - 15:30 at B - Fifth Avenue - Fixpoints Chair(s): Sam Tobin-Hochstadt

Big-step abstract interpreters are an approach to build static analyzers based on big-step interpretation. While big-step interpretation provides a number of benefits for the definition of an analysis, it also requires particularly complicated fixpoint algorithms because the analysis definition is a recursive function whose termination is uncertain. This is in contrast to other analysis approaches, such as small-step reduction, abstract machines, or graph reachability, where the analysis essentially forms a finite transition system between widened analysis states.

We show how to systematically develop sophisticated fixpoint algorithms for big-step abstract interpreters and how to ensure their soundness. Our approach is based on small and reusable fixpoint combinators that can be composed to yield fixpoint algorithms. For example, these combinators describe the order in which the program is analyzed, how deep recursive functions are unfolded and loops unrolled, or they record auxiliary data such as a (context-sensitive) call graph. Importantly, each combinator can be developed separately, reused across analyses, and can be verified sound independently. Consequently, analysis developers can freely compose combinators to obtain sound fixpoint algorithms that work best for their use case. We provide a formal metatheory that guarantees a fixpoint algorithm is sound if its composed from sound combinators only. We experimentally validate our combinator-based approach by describing sophisticated fixpoint algorithms for analyses of Stratego, Scheme, and WebAssembly.

Tue 5 Sep

Displayed time zone: Pacific Time (US & Canada) change

15:00 - 16:00
FixpointsICFP Papers and Events at B - Fifth Avenue
Chair(s): Sam Tobin-Hochstadt Indiana University
Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
ICFP Papers and Events
Sven Keidel TU Darmstadt, Germany, Sebastian Erdweg JGU Mainz, Tobias Hombücher JGU Mainz
More Fixpoints! (Functional Pearl)Functional Pearl
ICFP Papers and Events
Joachim Breitner unaffiliated
DOI Pre-print File Attached