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

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: |
[postscript] |