General Bindings and Alpha-Equivalence in Nominal Isabelle

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)

zbMATH Keywords

formal reasoninglambda-calculustheorem proversalpha-equivalencenominal Isabellevariable convention

Mathematics Subject Classification ID

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

• Unnamed Item
• HOL
• Twelf
• Nominal Isabelle
• Unbound
• Psi-calculi

This page was built for publication: General Bindings and Alpha-Equivalence in Nominal Isabelle