ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Tue 14 Oct 2025 16:50 - 17:15 at Peony West - Analyze This Chair(s): Jens Palsberg

Simple closure analysis (SCA) distills the essence of the machinery underlying guaranteed (near-)linear time constraint-based program analyses that emerged in the early 1990s. It involves three key steps. First, reduction to a constraint problem that captures abstract value flow in higher-order programming languages. Second, constraint normalization by instrumented unification closure. Finally, interpretation of the normalized constraints in the program analysis problem at hand.

In the present paper we revisit SCA and explain its original rationale of combining excellent asymptotic and practical run-time efficiency with guaranteed semantic robustness properties. We point out that SCA models induced flows bidirectionally, but keeps directional surface flow information. This preserves valuable directional flow information while breaking through the inherent quasi-cubic complexity of full closure analysis (0CFA), in which also induced flows are directional. We review some of the subsequent applications, extensions, and results on semantic robustness of SCA. We suggest that its modularity and the efficiency of its core data structure, a contracted and closed flow graph on abstract closures and structured data, be kept in mind for algorithmically efficient and semantically robust program analyses on large code bases.

This paper contains the original technical report on Simple Closure Analysis, with a few typographical changes and added explanations for clarification. It was posted on an FTP server at DIKU in 1992 and influenced several subsequent works, but was never submitted for publication (until now). It is a (very) late response to Olivier Danvy's original invitation to submit it to Higher Order Symbolic Computation with my heartfelt thanks for his encouragement.

Tue 14 Oct

Displayed time zone: Perth change

16:00 - 17:45
Analyze ThisOlivierFest at Peony West
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:00
25m
Talk
On the Structure of Abstract Interpretersfestschrift
OlivierFest
Wonyeol Lee POSTECH, Matthieu Lemerre Université Paris-Saclay - CEA List, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST
DOI
16:25
25m
Talk
Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_corefestschrift
OlivierFest
DOI
16:50
25m
Talk
Simple Closure Analysis Revisitedfestschrift
OlivierFest
Fritz Henglein University of Copenhagen
DOI
17:15
15m
Talk
Mixing transformation and symbolic execution with continuation for WebAssembly
OlivierFest
Guannan Wei Tufts University
17:30
15m
Talk
Data-Centric Functional Programming with First-Class Finite Maps and Tabulated Abstractions
OlivierFest
Tiark Rompf Purdue University