Nominal Techniques for the Specification of Languages with Binders

Abstract: The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. Nominal logic is a theory of first-order logic that axiomatizes the notions of fresh name, name swapping and abstraction from nominal sets, making it an ideal tool for the specification of the semantics of programming languages. In this talk, we will start by recalling the main concepts of nominal logic, and then we will show how to apply these ideas to specify calculi with binders. More precisely, we will introduce nominal syntax (including the notions of fresh atoms and alpha-equivalence), present matching and unification algorithms that take into account the alpha-equivalence relation, define nominal rewriting (a generalisation of first-order rewriting that provides in-built support for alpha-equivalence following the nominal approach) and give examples of application.

programming languageslogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic