Nominal 2


Title: Nominal 2
Authors: Christian Urban, Stefan Berghofer and Cezary Kaliszyk
Submission date: 2013-02-21

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.

  author  = {Christian Urban and Stefan Berghofer and Cezary Kaliszyk},
  title   = {Nominal 2},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2013,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: Incompleteness, Launchbury, Modal_Logics_for_NTS, Rewriting_Z