Abstract

Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
prover. It provides a proving infrastructure for reasoning about
programming language calculi involving named bound variables (as opposed to
de-Bruijn indices). In this paper we present an extension of Nominal
Isabelle for dealing with general bindings, that means term constructors
where multiple variables are bound at once. Such general bindings are
ubiquitous in programming language research and only very poorly supported
with single binders, such as lambda-abstractions. Our extension includes
new definitions of alpha-equivalence and establishes automatically the
reasoning infrastructure for alpha-equated terms. We also prove strong
induction principles that have the usual variable convention already built in.

BibTeX

@article{UK-LMCS12,
  author  = "Christian Urban and Cezary Kaliszyk",
  title   = "General Bindings and Alpha-Equivalence in Nominal {I}sabelle",
  journal = "Logical Methods in Computer Science",
  volume  = 8,
  number  = 2,
  pages   = "1--35",
  year    = 2012
}