Nominal techniques in Isabelle/HOL

DOI10.1007/s10817-008-9097-2zbMath1140.68061MaRDI QIDQ928672

Christian Urban

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

zbMATH Keywords

Lambda-calculus; Theorem provers; Nominal logic work

Mathematics Subject Classification ID

03B40: Combinatory logic and lambda calculus

Related Items

Psi-calculi in Isabelle, Nominal Isabelle, Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL, Mechanized Verification of CPS Transformations, The Isabelle Framework

Uses Software

• Isabelle
• Isabelle/HOL
• Isar
• PoplMark

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