Set-Based Analysis for Full Scheme and Its Use in Soft-Typing
Set-Based Analysis is an efficient and accurate program analysis for higher-order languages. It exploits an intuitive notion of approximation that treats program variables as sets of values. We present a new derivation of set-based analysis, based on a reduction semantics, that substantially simplifies previous formulations. Most importantly, the derivation easily extends from a functional core language to include imperative features such as assignments and first-class continuations, and supports the first correctness proof of set-based analysis for these imperative features. The paper includes an implementation of the derived analysis for a Scheme-like language, and describes a soft-typing algorithm that eliminates type-checks based on the information produced by the analysis.