General Binding in Nominal Isabelle

Abstract: Nominal Isabelle is a definitional extension of the Isabelle/HOL theoremprover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (asopposed to de-Bruijn indices). We have extended Nominal Isabelle so that it can deal with terms which bind multiple variables at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. In this talk I will present the new definition of alpha-equivalence behind the extension and show how to establish automatically a reasoning infrastructure for the more general terms.