Nominal 2

Title:	Nominal 2
Authors:	Christian Urban, Stefan Berghofer and Cezary Kaliszyk
Submission date:	2013-02-21
Abstract:	Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs, especially in proofs by structural and rule induction. Nominal Isabelle is designed to make such proofs easy to formalise: it provides an infrastructure for declaring nominal datatypes (that is alpha-equivalence classes) and for defining functions over them by structural recursion. It also provides induction principles that have Barendregt’s variable convention already built in. This entry can be used as a more advanced replacement for HOL/Nominal in the Isabelle distribution.
BibTeX:	@article{Nominal2-AFP, author = {Christian Urban and Stefan Berghofer and Cezary Kaliszyk}, title = {Nominal 2}, journal = {Archive of Formal Proofs}, month = feb, year = 2013, note = {\url{http://isa-afp.org/entries/Nominal2.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	FinFun
Used by:	Goedel_HFSet_Semanticless, Incompleteness, LambdaAuth, Launchbury, Modal_Logics_for_NTS, Rewriting_Z, Robinson_Arithmetic
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.