Abstract

Structural Operational Semantics (SOS) is one of the most natural ways for providing programming languages with a formal semantics. In this talk, we focus on Nominal SOS, a formalization of SOS with explicit syntax and primitives for the specification of languages with binders, as lambda-calculus and pi-calculus. In SOS, bisimilarity is typically the most suitable equivalence relation over programs. We offer a syntactic method for proving that bisimilarity is a congruence for languages defined in Nominal SOS, i.e. that bisimilarity is preserved by all the operators of the language being defined. We show the applicability of the method by recovering classic results, most notably that Sangiorgi’s open bisimilarity is a congruence for pi-calculus. (Remark: This is a nearly finished, but unfinished work.)