A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages

In this paper we describe the promoted tyft/tyxt rule format for defining higher-order languages. The rule format is a conservative generalization of Groote and Vaandrager's tyft/tyxt format which allows terms as labels on transitions in rules. We prove that bisimulation is a congruence for any language defined in promoted tyft/tyxt format and demonstrate the usefulness of the rule format by presenting promoted tyft/tyxt definitions for the lazy -calculus, CHOCS and the ß-calculus. 1 Introduction For a program language definition that uses bisimulation as the notion of equivalence, it is desirable for the bisimulation relation to be compatible with the language constructs; i.e. bisimulation to be a congruence. Several rule formats have been defined, so that as long as a definition satisfies certain syntactic constraints, then the defined bisimulation relation is guaranteed to be a congruence. Unfortunately the existing rule formats have not been very useful for defining languages wit..