Strictness analysis and denotational abstract interpretation

AbstractA theory of abstract interpretation (P. Cousot and R. Cousot, in “Conf. Record, 4th ACM Symposium on Principles of Programming Languages,” 1977) is developed for a typed λ-calculus. The typed λ-calculus may be viewed as the “static” part of a two-level denotational metalanguage for which abstract interpretation was developed by F. Nielson (Ph.D. thesis, University of Edinburgh, 1984; in “Proceedings, STACS 1986,” Lecture Notes in Computer Science, Vol. 210, Springer-Verlag, New York/Berlin, 1986). The present development relaxes a condition imposed there and this sufices to make the framework applicable to strictness analysis for the λ-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; P. Cousot and R. Cousot, in “Conf. Record, 6th ACM Symposium on Principles of Programming Languages,” 1979) semantics exists, thus answering a problem left open by G. L. Burn, C. L. Hankin and S. Abramsky (Sci. Comput. Programming7 (1986), 249–278)