A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial - Extended abstract

A multi-stage computation is one involving more than one stage of execution . MetaML is a language for programming multi-stage computations. Previous s tudies presented big-step semantics, categorical semantics, and sound type systems for MetaML. In this paper, we report on a confluent and sound reduc tion semantics for untyped call-by name (CBN) MetaML. The reduction semanti cs can be used to formally justify some optimization performed by a CBN Met aML implementation. The reduction semantics demonstrates that non-trivial e qualities hold for object-code, even in the untyped setting. The paper also emphasizes that adding intensional analysis (that is, taking-apart object programs) to MetaML remains an interesting open problem.