Nominal techniques in Isabelle/HOL
type: Item
instance of: scholarly article
title: Nominal techniques in Isabelle/HOL
zbMATH Open document ID: 1140.68061
author: Christian Urban
published in: Journal of Automated Reasoning
publication date: 2008-06-11T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 5287724
zbMATH Keywords: Lambda-calculus
zbMATH Keywords: Nominal logic work
zbMATH Keywords: Theorem provers
describes a project that uses: Isar
describes a project that uses: Isabelle/HOL
describes a project that uses: Isabelle
describes a project that uses: PoplMark
MaRDI profile type: Publication
full work available at URL: s10817-008-9097-2
OpenAlex ID: W2037026294
cites work: Q4484329
cites work: Engineering formal metatheory
cites work: Theorem Proving in Higher Order Logics
cites work: The lambda calculus, its syntax and semantics
cites work: Formalising the π-Calculus Using Nominal Logic
cites work: Q3024831
cites work: Higher order unification via explicit substitutions
cites work: A new approach to abstract syntax with variable binding
cites work: Q3994895
cites work: Disjunction and existence under implication in elementary intuitionistic formalisms
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
cites work: Nominal logic, a first order theory of names and binding
cites work: Alpha-structural recursion and induction
cites work: Q2723408
cites work: Parallel reductions in \(\lambda\)-calculus
cites work: The design and implementation of typed scheme
cites work: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
cites work: Barendregt’s Variable Convention in Rule Inductions
cites work: Nominal unification
cites work: Automated Deduction – CADE-20
cites work: Structured Induction Proofs in Isabelle/Isar
DOI: 10.1007/S10817-008-9097-2
Recommended article: Automated Deduction – CADE-20
Recommended article: Nominal reasoning techniques in Coq (extended abstract)
Recommended article: A New Foundation for Nominal Isabelle
Recommended article: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
Recommended article: Q4823141
Recommended article: Higher-Order Abstract Syntax in Isabelle/HOL
Recommended article: Nominalization, predication and type containment
Recommended article: A consistent foundation for Isabelle/HOL
Recommended article: A Consistent Foundation for Isabelle/HOL
Recommended article: General bindings and alpha-equivalence in Nominal Isabelle
description: scientific article; zbMATH DE number 5287724