Operational Semantics Using the Partiality Monad

Operational Semantics Using the Partiality Monad
Talk given at DTP 2010, Edinburgh, 2010-07-09. [pdf, accompanying code]

Abstract

An operational semantics for a partial language is usually defined as a relation, either in the form of a small-step semantics or as a big-step semantics. I will discuss an alternative approach: by using the partiality monad one can define the semantics as a total function. This makes it possible to state compiler correctness in a way which I find easier to understand (and hence get right). Instead of separate statements dealing with termination, non-termination, crashes, raised exceptions, and so on, one can get by with a single, uniform statement.