A Conservative Look at Operational Semantics with Variable Binding

We set up a formal framework to describe transition system specifications in the style of Plotkin. This framework has the power to express many-sortedness, general binding mechanisms and substitutions, among other notions such as negative hypotheses and unary predicates on terms. The framework is used to present a conservativity format in operational semantics, which states sufficient criteria to ensure that the extension of a transition system specification with new transition rules does not affect the semantics of the original terms.

• Type: Journal
• Year: 1998
• Where: IANDC
• Authors: Wan Fokkink, Chris Verhoef
• Keywords: Formal Framework, IANDC 1998, Negative Hypotheses, Transition System Specification