Flag-Based Big-Step Semantics

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.

To appear in The Journal of Logical and Algebraic Methods in Programming, Special Issue: 26th Nordic Workshop for Programming Theory, 2014