Nominal 2 (Q7361006)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Nominal2
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Nominal 2 |
AFP entry Nominal2 |
Statements
21 February 2013
0 references
Christian Urban
0 references
Stefan Berghofer
0 references
Cezary Kaliszyk
0 references
Nominal 2 (English)
0 references
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.
0 references
