Operational Semantics Using the Partiality Monad

Operational Semantics Using the Partiality Monad
Agda Implementors' Meeting XI, Awaji Yumebutai, 2010-03-24. (Slightly edited.) [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 three separate statements, referring to terminating, non-terminating and undefined (crashing) computations, one can get by with a single, uniform statement.