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 three separate statements, referring to terminating, non-terminating and undefined (crashing) computations, one can get by with a single, uniform statement.Nils Anders Danielsson
Last updated Wed Mar 24 08:51:33 CET 2010.