Strictness Analysis and Denotational Abstract Interpretation

A theory of abstract interpretation () is developed for a typed lambda-calculus. The typed lambda-calculus may be viewed as the ''static'' part of a two-level denotational metalanguage for which abstract interpretation was developed by ). The present development relaxes a condition imposed there and this sufices to make the framework applicable to strictness analysis for the lambda-calculus. This shows the possibility of a general theory for the analysis of functional programs and it gives more insight into the relative precision of the various analyses. In particular it is shown that a collecting (static; ) semantics exists, thus answering a problem left open by , 249-278).