### 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.

### License

BSD License

### Topics

- Tools

### Session Nominal2

- Nominal2_Base
- Nominal2_Abs
- Nominal2_FCB
- Nominal2
- Atoms
- Eqvt

### Depends on

- Code Generation for Functions as Data

### Used by

- MiniSail - A kernel language for the ISA specification language SAIL
- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part II
- Robinson Arithmetic
- Formalization of Generic Authenticated Data Structures
- Modal Logics for Nominal Transition Systems
- The Z Property
- Gödel’s Incompleteness Theorems
- The Correctness of Launchbury’s Natural Semantics for Lazy Evaluation

## Cite

×

Nominal2-AFP

    @article{Nominal2-AFP,
      author  = {Christian Urban and Stefan Berghofer and Cezary Kaliszyk},
      title   = {Nominal 2},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Nominal2.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Apr 24, 2016 : Isabelle2016
- Nov 17, 2013 : Isabelle2013-1
- Feb 24, 2013 : Isabelle2013