By Casper Bach Poulsen and Peter D. Mosses
Abstract:
Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.
The material listed below accompanies the article submitted to the NWPT 2014 special issue of the Journal of Logical and Algebraic Methods in Programming.