Strictness and Totality Analysis

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    We define a novel inference system for strictness and totality analysis for the simply-typed lazy lambda-calculus with constants and fixpoints. Strictness information identifies those terms that definitely denote bottom (i.e. do not evaluate to WHNF) whereas totality information identifies those terms that definitely do not denote bottom (i.e. do evaluate to WHNF). The analysis is presented as an annotated type system allowing conjunctions at ?top-level? only. We give examples of its use and prove the correctness with respect to a natural-style operational semantics.
    Original languageEnglish
    JournalScience of Computer Programming
    Volume31
    Issue number1
    Pages (from-to)113-145
    ISSN0167-6423
    DOIs
    Publication statusPublished - 1998
    Event1st International Static Analysis Symposium (SAS 94) - Namur, Belgium
    Duration: 27 Sep 199429 Sep 1994
    Conference number: 1

    Conference

    Conference1st International Static Analysis Symposium (SAS 94)
    Number1
    CountryBelgium
    CityNamur
    Period27/09/199429/09/1994

    Keywords

    • Strictness and totality analysis
    • Top-level conjunction types
    • Natural-style operational semantics
    • Annotated type system

    Cite this