Nominal Techniques for Reasoning about Formal Languages

When reasoning about formal languages, dealing with binding constructs is of-ten delicate and error-prone, in particular when proving properties by structural induction. This course describes a general framework for representing formal languages involving binders and reasoning modulo renaming of bound names. The framework is based on the operation of swapping of names and on the notion of equivariant predicates (that is predicates that are invariant under the swapping operation); the framework provides rigorous proving techniques that are pleas-antly close to informal practice, in contrast with more sophisticated techniques such as de-Bruijn indices and higher-order abstract syntax. Examples explaining the techniques will be taken from the lambda-calculus. Acknowledgements: These overview notes draw heavily upon the papers [2, 3, 5, 6, 7, 8] and several other sources from the FreshML-project. I am most grateful to Andrew Pitts for all his help with preparing these notes. The notes also benefited much from the conversations with Christine Tasson. Any errors are my own work. 1