Modular semantics

Action semantics and modular monadic semantics are two independent approaches to the problem of specifying programming language semantics. Action semantics, developed by Mosses, is intended to be a system allowing "useful semantic descriptions of realistic programming languages"; its worth has been demonstrated by the existence of action semantic descriptions of a number of relatively large languages. Modular monadic semantics is a more recent system developed by Espinosa and Liang, Hudak and Jones based on work done by Moggi; it is essentially an extension of concept of monads currently enjoying wide use for the represention of state in functional languages.

In this work we present modular monadic action semantics, a system that combines the best features of action semantics and modular monadic semantics. Modular monadic action semantics replaces the structural operational semantics that formalises action semantics with a modular monadic semantics. This replacement provides the flexibility to modify or delete existing facets of action semantics or to add entirely new ones, and will allow the use of the theories of modular monadic semantics and of denotational semantics to theorise about actions.

We have implemented modular monadic action semantics in the functional language Gofer, and in this work we discuss a number of issues that arose during the implementation relating to both action semantics and modular monadic semantics. The implementation clarified a number of facts relating to the structure of action semantics; it also contributed two new constructs to modular monadic semantics, representing I/O and parallelism. We demonstrate some of the power of modular monadic action semantics by adding a continuational facet to action semantics, allowing representation of the call/cc operation.

Further information can be found on my Masters thesis page.

Document research/mmas revised 03-Apr-2005.
Generated by PMT v1.1.