Under consideration for publication in J. Functional Programming 1 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. In this paper, we present a novel calculus for staged computation with the notion of type safety as outlined above. The type system is based on the necessity operator � from constructive modal logic. We index the modal operator with a set C of names, so that the type �CA classifies expressions of type A that belong to the late stage, and whose free names are in the set C.