Substructural Operational Semantics as Ordered Logic Programming

We describe a substructural logic with ordered, linear, and persistent propositions and then endow a fragment with a committed choice forward-chaining operational interpretation. Exploiting higher-order terms in this metalanguage, we specify the operational semantics of a number of object language features, such as call-by-value, call-by-name, call-by-need, mutable store, parallelism, communication, exceptions and continuations. The specifications exhibit a high degree of uniformity and modularity that allows us to analyze the structural properties required for each feature in isolation. Our substructural framework thereby provides a new methodology for language specification that synthesizes structural operational semantics, abstract machines, and logical approaches.