Capture-Avoiding Substitution as a Nominal Algebra

DOI10.1007/11921240_14zbMath1152.68454OpenAlexW2131034879MaRDI QIDQ3525150

Aad Mathijssen, Murdoch James Gabbay

Publication date: 11 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11921240_14

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42)

Related Items (11)

Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Nominal Matching and Alpha-Equivalence ⋮ Capture-avoiding substitution as a nominal algebra ⋮ a-Logic With Arrows ⋮ Matching and alpha-equivalence check for nominal terms ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness ⋮ A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets ⋮ Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables ⋮ Two-level Lambda-calculus ⋮ Abstract Syntax: Substitution and Binders

This page was built for publication: Capture-Avoiding Substitution as a Nominal Algebra