General Bindings and Alpha-Equivalence in Nominal Isabelle
Abstract elided by the publisher.
Related papers
- Nominal Matching Logic with Fixpoints CPP 2025
- Bindings as bounded natural functors POPL 2019
- Nominal Recursors as Epi-Recursors POPL 2024
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem CPP 2011
- Towards nominal computation POPL 2012
- Rebound: Efficient, Expressive, and Well-Scoped Binding Haskell 2025
- A Fresh Approach to Representing Syntax with Static Binders in Functional Programming ICFP 2001
- Hashing modulo alpha-equivalence PLDI 2021