Operational Semantics Using the Partiality Monad
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.Nils Anders Danielsson
Last updated Fri Jul 9 13:16:16 UTC 2010.