ABSTRACT.
Monadic metalanguages had been proposed by Moggi (in 1990) as a way to make explicit the distinction between values and computations, and provide a better structuring of "denotational semantics".

Since 1990, Wadler (and others) have used monads to incorporate "computational effect" in the pure functional language Haskell without giving up equational properties useful in optimizations by Haskell compilers. Indeed, monadic metalanguages are a "conservative extensions" of (typed) lambda calculi.

Recently (2003) Fagorzi and Moggi proposed a general pattern for the operational semantics of monadic metalanguages inspired by Berry and Boudol's Chemical Abstract Machine, namely it consists of two parts: local (semantics preserving) simplification rules, and computation steps executed in a "deterministic order" (because they may have side-effects).

Monadic metalanguages might be useful

• to reconcile "mathematical reasoning" and "programming", a problem stressed in the position statement by Mohring and Sheard, by explicitly extending typed calculi of a "logical nature" with "computational types" and "effects";
• to aid program transformation (an important issue mentioned by several members, e.g. Visser), by providing "cheap transformations" in the form of "simplification rules" (more global transformations do not come for free);

We give two examples of monadic metalanguages. The first is inspired by MetaML (Sheard and Taha), and it indicates how to add "staging" to a pre-existing monadic monadic metalanguage. The second in loosely inspired by Nanevski&Pfenning's nuBox calculus for meta-programming with names and necessity (but revised in the light of Ancona&Zucca's calculus for module systems, and Pitts&Gabbay's FreshML).

MetaML and nuBox represent different approaches to the same problem: combine (safely) execution of "closed code", and manipulation of "open code" (as in partial evaluation).

Casting them as monadic metalanguages seems to help in understanding the trade-offs (but so far we have not been able to compare their "expressiveness", e.g. by giving formal translations).