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