|Who||Martin Schwenke, Brendan Mahony|
|Where||International Refinement Workshop and Formal Methods Pacific 1998, pages 324–333|
Expression refinement semantics are often complex. In particular, semantics for the relatively simple notion of function application are often disproportionately complex. Monads are frequently championed as the `right' tool for structuring the semantics of function application. In this paper, we consider the interaction between monadic semantics and refinement semantics. We demonstrate that a monad extended with a refinement ordering becomes an elegant tool for structuring the semantics of expression refinement. We do not claim that using monads to structure the semantics of function application is a new idea, nor do we introduce novel semantic models for non-deterministic languages. We simply demonstrate that the structure provided by monads ensures a consistent semantic approach. We illustrate this further by adding a facility for output to one of our languages.
Note:This version of the paper contains the following fixes compared to the originally published version:
PDF (144 KB)