General Bindings and Alpha-Equivalence in Nominal Isabelle
From MaRDI portal
Publication:5892493
DOI10.1007/978-3-642-19718-5_25zbMath1326.68265arXiv1206.0136OpenAlexW1495561703WikidataQ108482189 ScholiaQ108482189MaRDI QIDQ5892493
Cezary Kaliszyk, Christian Urban
Publication date: 19 May 2011
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1206.0136
Related Items
HOCore in Coq ⋮ A formalized general theory of syntax with bindings ⋮ Unnamed Item ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ A formalized general theory of syntax with bindings: extended version ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ Unnamed Item ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ Nominal Isabelle ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Mechanizing the Metatheory of mini-XQuery
Uses Software
Cites Work
- Unnamed Item
- External and internal syntax of the \(\lambda \)-calculus
- Nominal logic, a first order theory of names and binding
- The locally nameless representation
- Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
- Scrap your nameplate
- Mechanizing the metatheory of LF
- Towards a mechanized metatheory of standard ML
- The design and implementation of typed scheme
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- ΠΣ: Dependent Types without the Sugar
- Ott: Effective tool support for the working semanticist
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- A New Foundation for Nominal Isabelle
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Psi-calculi in Isabelle
