Taha W. A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trival. Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation. (34-43). https://doi.org/10.1145/328690.328697