| 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. |