Staged Computation with Names and Necessity

Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate, at run time, the code for the late stages. The late stages may then be explicitly evaluated when appropriate. A type system for staging should ensure that only well-typed expressions are generated, and that only expressions with no free variables are permitted for evaluation