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

In this paper we describe the promoted tyft tyxt rule format for de ning higher-order languages. The rule format is a generalization of Groote and Vaandrager's tyft tyxt format in which terms are allowed as labels on transitions in rules. We prove that bisimulation is a congruence for any language de ned in promoted tyft tyxt format and demonstrate the usefulness of the rule format by presenting promoted tyft tyxt de nitions for the lazy -calculus, CHOCS and the -calculus.

• Type: Conference
• Year: 1998
• Where: LICS
• Authors: Karen L. Bernstein
• Keywords: Automated Reasoning, LICS 1998, Promoted Tyft Tyxt, Rule Format, Tyft Tyxt Format