Title: A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages
Published: July 1997
Authors: Karen L. Bernstein
Abstract: In this paper we describe promoted-tyft, a syntactic rule format for defining higher-order languages. The rule format is a conservative generalization of Groote and Vaandrager's tyft format that allows terms as labels on transitions in rules. We give a direct proof that bisimulation is a congruence for any language defined in promoted-tyft format, and demonstrate the expressiveness of the rule format by presenting a promoted-tyft definition for the lazy lambda-calculus and an outline of a promoted-tyft definition for the pi-calculus.
Full Paper: N/A