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
Topics
Session Nominal2
Depends on
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