Capture-avoiding substitution as a nominal algebra

DOI10.1007/s00165-007-0056-1zbMath1152.68025OpenAlexW2168547990MaRDI QIDQ939160

Aad Mathijssen, Murdoch James Gabbay

Publication date: 21 August 2008

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-007-0056-1

zbMATH Keywords

SubstitutionBindingCapture-avoidanceNominal algebraNominal rewritingNominal techniquesOmega-completeness

Mathematics Subject Classification ID

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

Related Items (15)

Unnamed Item ⋮ Encoding abstract syntax without fresh names ⋮ Nominal syntax with atom substitutions ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Alpha equivalence equalities ⋮ Fixed-Point Constraints for Nominal Equational Unification ⋮ a-Logic With Arrows ⋮ Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax ⋮ 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 ⋮ The lambda-context calculus (extended version) ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Higher-order rewrite systems and their confluence
• An algebraic generalization of Frege structures -- binding algebras
• Combinatory reduction systems: Introduction and survey
• On the algebraic models of lambda calculus
• Nominal unification
• Nominal rewriting
• Capture-Avoiding Substitution as a Nominal Algebra
• A Formal Calculus for Informal Equality with Binding
• Axiomatization of polynomial substitution algebras
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The Lattice of Lambda Theories
• On the Notion of Substitution

This page was built for publication: Capture-avoiding substitution as a nominal algebra