We introduce a new proof technique for showing the correctness of 0CFA-like analyses with respect to small-step semantics. Weillustrate the technique by proving the correctness of 0CFA for the pureλ-calculus under arbitrary β-reduction. This result was claimed by Palsbergin 1995; unfortunately, his proof was flawed. We provide a correct proof of this result, using a simpler and more general proof method. We illustrate the extensibility of the new method by showing the correctness of an analysis for the Abadi-Cardelli object calculus under small-step semantics.
CITATION STYLE
Wand, M., & Williamson, G. B. (2002). A modular, extensible proof method for small-step flow analyses. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2305, pp. 213–227). Springer Verlag. https://doi.org/10.1007/3-540-45927-8_16
Mendeley helps you to discover research relevant for your work.