General Bindings and Alpha-Equivalence in Nominal Isabelle
From MaRDI portal
Publication:5891628
DOI10.2168/LMCS-8(2:14)2012zbMath1242.68283WikidataQ108482184 ScholiaQ108482184MaRDI QIDQ5891628
Christian Urban, Cezary Kaliszyk
Publication date: 3 July 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Related Items (18)
A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The Role of Indirections in Lazy Natural Semantics ⋮ Nominal unification with atom-variables ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ The adequacy of Launchbury's natural semantics for lazy evaluation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ αCheck: A mechanized metatheory model checker ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Psi-calculi in Isabelle ⋮ Rewriting with generalized nominal unification ⋮ Generic Authenticated Data Structures, Formally. ⋮ Binding operators for nominal sets ⋮ Term-generic logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Nominal unification with letrec and environment-variables
Uses Software
This page was built for publication: General Bindings and Alpha-Equivalence in Nominal Isabelle
