Abstract

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 λ-calculus this distinction is formalized by a two-level λ-calculus. We present an algorithm for static analysis of the binding times of a typed λ-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 λ-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.