Automatic Binding Time Analysis for a Typed Lambda-Calculus
Abstract
For a typed λ-calculus we develop an algorithm that, given some partial information about what must happen at run-time, will work out what actually can be computed at compile-time and what must be deferred to run-time.