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{https://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.