Two-Level Semantics and Abstract Interpretation

Two-level semantics is a variant of Scott/Strachey denotational semantics in which the concept of binding time is treated explicitly. This is done by formally distinguishing between those computations that take place at run-time and those that take place at compile-time. Abstract interpretation is concerned with the (preferably automatic) analysis of programs.

The main purpose of these analyses is to find information that may assist in the efficient implementation of the programs. Abstract interpretation is thus related to data flow analysis, partial evaluation and other program analysis methods. Its unique flavour is the insistence on formal proofs of correctness and the methods used to establish these.

This paper develops a theory of abstract interpretation for two-level denotational definitions. There are three ingredients in this. First a framework for proving the correctness of analyses is developed. This may also be used to compare the precision of various analyses. Next it is shown that, given a choice of properties of programs, one may specify a most precise analysis (or best induced analysis).

This may also be used to investigate the collecting semantics (or static semantics). Finally, it is shown how to modify the most precise analysis in order to obtain an implementable analysis where one trades off precision for implementability