Formalising languages with binders (such as programming languages and logics) within a logical framework with zero representational distance (i.e., the calculus and its representation look the same) poses non-trivial challenges, including: faithful representation of syntax and binding operators; support for calculus-specific equivalences; faithful representation of the language dynamics (operational semantics); and generation of correct-by-construction implementations.

We show how to use rewriting logic to meet these challenges. More precisely, we show how a general notion of binder signature can be axiomatised in rewriting logic following the nominal approach, and we propose a general methodology to specify languages with binders, including their structural congruences and operational semantics. We also show how rewriting logic methods provide executable specifications of languages with binders. We use the pi-calculus as a running example because it illustrates well the above-mentioned challenges.

(Joint work with Jose Meseguer)