Multi-stage programming provides a new paradigm for constructing efficient solutions to complex problems. Techniques such
as program generation, multi-level partial evaluation, and run-time code generation respond to the need for general purpose
solutions which do not pay run-time interpretive overheads. This paper provides a foundation for the formal analysis of one
such system.
We introduce a multi-stage language and present its axiomatic and reduction semantics. Our axiomatic semantics is an extension
of the call-by-value λ-calculus with staging constructs. We show that staged-languages can “go Wrong” in new ways, and devise
a type system that screens out such programs. Finally, we present a proof of the soundness of this type system with respect
to the reduction semantics.
The research reported in this paper was supported by the USAF Air Materiel Command, contract # F19628-93-C-0069, and NSF Grant
IRI-9625462.