Strictness Analysis and Denotational Abstract Interpretation

Flemming Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review


    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).
    Original languageEnglish
    JournalInformation and Computation
    Issue number1
    Pages (from-to)29-92
    Publication statusPublished - 1988


    Dive into the research topics of 'Strictness Analysis and Denotational Abstract Interpretation'. Together they form a unique fingerprint.

    Cite this