By Yuichiro Hanada and Atsushi Igarashi. To appear in Proceedings of the International Symposium on Functional and Logic Programming (FLOPS2014), volume 8475 of Lecture Notes in Computer Science, pages 103-118, Kanazawa, Japan, June 2014. Springer-Verlag.
We develop yet another typed multi-stage calculus λ|>%. It extends Tsukada and Igarashi's λ|> 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 λ|>% gives a sufficient condition when residual programs can be safely generated, making λ|>% more suitable for writing generating extensions than previous multi-stage calculi.
$Date: $