Automatic Binding Time Analysis for a Typed Lambda-Calculus

Hanne Riis Nielson, Flemming Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review


    A binding time analysis imposes a distinction between the computations to be performed early (e.g. at compile-time) and those to be performed late (e.g. at run-time). For the lambda-calculus this distinction is formalized by a two-level lambda-calculus. The authors present an algorithm for static analysis of the binding times of a typed lambda-calculus with products, sums, lists and general recursive types. Given partial information about the binding times of some of the subexpressions it will complete that information such that (i) early bindings may be turned into late bindings but not vice versa, (ii) the resulting two-level lambda-expression reflects our intuition about binding times, e.g. that early bindings are performed before late bindings, and (iii) as few changes as possible have been made compared with the initial binding information. The results can be applied in the implementation of functional languages and in semantics directed compiling
    Original languageEnglish
    JournalScience of Computer Programming
    Issue number2
    Pages (from-to)139-176
    Publication statusPublished - 1988


    Dive into the research topics of 'Automatic Binding Time Analysis for a Typed Lambda-Calculus'. Together they form a unique fingerprint.

    Cite this