01/07/2002:
Eugenio Moggi (Univ. di Genova)
A Monadic Multi-Stage Metalanguage
Résumé
We introduce a monadic multi-stage metalanguage, for
describing "staged" computations. The metalanguage allows computation
within the scope of (certain) binders, a feature which is needed for
run-time code generation, and thus has to cope with scope extrusion
problems.
On the metalanguage we define a simplification relation, which induces
a congruence on terms, and a transition relation modeling a
"computation step".
We show how the metalanguage can account for a multi-stage language, like
MetaML, and provide "multilingual" support.