Strictness Analysis and Denotational Abstract Interpretation

Flemming Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    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
    Volume76
    Issue number1
    Pages (from-to)29-92
    ISSN0890-5401
    Publication statusPublished - 1988

    Fingerprint

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

    Cite this