Nominal techniques in Isabelle/HOL
From MaRDI portal
Publication:928672
DOI10.1007/s10817-008-9097-2zbMath1140.68061MaRDI QIDQ928672
Publication date: 11 June 2008
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-008-9097-2
03B40: Combinatory logic and lambda calculus
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A new approach to abstract syntax with variable binding
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- The lambda calculus, its syntax and semantics
- Isabelle/HOL. A proof assistant for higher-order logic
- Higher order unification via explicit substitutions
- Nominal unification
- Nominal logic, a first order theory of names and binding
- Engineering formal metatheory
- The design and implementation of typed scheme
- Alpha-structural recursion and induction
- Barendregt’s Variable Convention in Rule Inductions
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Disjunction and existence under implication in elementary intuitionistic formalisms
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Structured Induction Proofs in Isabelle/Isar
- Formalising the π-Calculus Using Nominal Logic
- Parallel reductions in \(\lambda\)-calculus