Relatively Complete Pushdown Analysis of Escape Continuations
Escape continuations are weaker than full, first-class continuations but nevertheless can express many common control operators. Although language and compiler designs profitably leverage escape continuations, all previous approaches to analyze them statically in a higher-order setting have been ad hoc or imprecise. We present MCCFA2, a generalization of CFA2 that analyzes them with pushdown precision in their most-general form. In particular, the summarization algorithm of MCCFA2 is both sound and complete with respect to a conservative extension of CFA2’s abstract semantics. We also sketch an integration into our framework of Vardoulakis and Shivers’ technique to handle first-class continuations that offers the full precision of MCCFA2 to uses of them as mere escape continuations.
Sun 13 JanDisplayed time zone: Belfast change
16:00 - 17:30
|Demand Control-Flow Analysis|
|Effect-driven Flow Analysis|
|Relatively Complete Pushdown Analysis of Escape Continuations|