On Cross-Stage Persistence in Multi-Stage Programming

We develop yet another typed multi-stage calculus. lambda((sic)%). It extends Tsukada and Igarashi's. lambda((sic)) with cross-stage persistence and is equipped with all the key features that MetaOCaml-style multi-stage programming supports. It has an arguably simple, substitution-based full-reduction semantics and enjoys basic properties of subject reduction, confluence, and strong normalization. Progress also holds under an alternative semantics that takes staging into account and models program execution. The type system of lambda((sic)%) gives a sufficient condition when residual programs can be safely generated, making. lambda((sic)%) more suitable for writing generating extensions than previous multi-stage calculi.