1 Computer Science and Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark2 Department of Informatics and Mathematical Modeling, Technical University of Denmark3 Department of Applied Mathematics and Computer Science, Technical University of Denmark
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).
Information and Computation, 1988, Vol 76, Issue 1, p. 29-92