A Congruence Format for Name-passing Calculi

We define and use a SOS-based framework to specify the transition systems of calculi with name-passing properties. This setting uses proof-theoretic tools to take care of some of the difficulties specific to name-binding and make them easier to handle in proofs. The contribution of this paper is the presentation of a format that ensures that open bisimilarity is a congruence for calculi specified within this framework, extending the well-known tyft/tyxt format to the case of name-binding and name-passing. We apply this result to the -calculus in both its late and early semantics. Key words: Structural operational semantics, rule formats, name-binding, name-mobility, open bisimulation.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Axelle Ziegler, Dale Miller, Catuscia Palamidessi
• Keywords: ENTCS 2006, SOS-based Framework, Transition Systems, Uses Proof-theoretic Tools