Automatic Binding Time Analysis for a Typed Lambda-Calculus

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