Automatic Binding Time Analysis for a Typed Lambda-Calculus

Publication: Research - peer-reviewJournal article – Annual report year: 1988

View graph of relations

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
StatePublished - 1988
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 3972947