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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: Incompleteness, Launchbury, Modal_Logics_for_NTS, Rewriting_Z
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.