In denotational semantics, programs are explained in terms of abstract
mathematical entities, called ``denotations,'' which model their
implementation-independent behaviour. In this context, formal
metalanguages can be used to link programs and their denotations:
on one side they provide a language for addressing elements of
mathematical structures, while on the other they provide a formal
framework in which programs can be interpreted by means of translations.
<p>
How tightly should a metalanguage match the mathematical objects it
describes and in what detail should it represent the structure of
computation? In recent years, E. Moggi proposed the use of monads
to represent notions of computation abstractly and a formal
metalanguage to match the categorical semantics. This approach goes
one step towards the identification of abstract reasoning principles
for computer applications. It also has a pragmatical significance,
because abstraction is a basic ingredient to achieve modularity.
<p>
We give a basic introduction to the mathematics of monads, show the 
correspondence with algebraic theories, present examples and survey
applications in computer science and formal specification.