ICE-TCS seminar: Matteo Cimini, Nominal SOS: A Framework for Structural Operational Semantics with Binders

  • 30.3.2012, 14:00 - 15:00

Speaker: Matteo Cimini

When: Friday, March 30th, 2pm

Where: V-109
Title: Nominal SOS: A Framework for Structural Operational Semantics with Binders.

Abstract:  Structural Operational Semantics (SOS) is one of the most natural ways for providing programming languages with a formal semantics. In many such languages, the concepts of variables and binders are essential ingredients. However, the SOS framework lacks a dedicated account for these concepts. In this talk, we present Nominal SOS, an SOS based framework with special syntax and primitives for the definition of languages with variables and binders. The framework is based on the Nominal Logic of Gabbay and Pitts, hence the adjective "nominal". We provide evidence that the framework is expressive enough to model interesting calculi. For instance, we will show a formulation of the $\lambda$-calculus and the $\pi$-calculus within Nominal SOS. We will present a suitable notion of bisimilarity that is aware of binding and we will see how some notorious program equivalence relations from the theory of the $\lambda$-calculus and the $\pi$-calculus relate to this notion. We will also discuss our future plans in the context of Nominal SOS.