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 Jan
|16:00 - 16:30|
|16:30 - 17:00|
|17:00 - 17:30|