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.

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Frank Pfenning, Robert J. Simmons
• Keywords: Computer Science, Forward-chaining Operational Interpretation, LICS 2009, Operational Semantics, Structural Operational Semantics