Strictness analysis and denotational abstract interpretation

Publisher Website
Google Scholar
Abstract
A theory of abstract interpretation [CoCo79] is developed for a typed &lgr;-calculus. The typed &lgr;-calculus is the “static” part of a two-level denotational metalanguage for which abstract interpretation was developed in [Nie86]. The present development relaxes a condition imposed in [Nie86] and this suffices to make the framework applicable to strictness analysis for the &lgr;-calculus. This shows the possibility of a general theory (and hence a system) for the analysis of functional programs. Furthermore, it gives more insight into the relative precision of the various analyses. In particular, it is shown that a collecting (static [CoCo79]) semantics exists, thus answering a problem left open in [BHA86].

This publication has 0 references indexed in Scilit: