Matching and alpha-equivalence check for nominal terms

DOI10.1016/j.jcss.2009.10.003zbMath1206.68159OpenAlexW2052280100MaRDI QIDQ980937

Maribel Fernández, Christophe Calvès

Publication date: 8 July 2010

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2009.10.003

zbMATH Keywords

matchingbindersalpha-equivalencenominal terms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ On solving nominal disunification constraints ⋮ Nominal equational problems ⋮ Checking overlaps of nominal rewriting rules ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Formalising nominal C-unification generalised with protected variables

Uses Software

• OCaml
• Freshml
• HNT

Cites Work

• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• A polynomial nominal unification algorithm
• Combinatory reduction systems: Introduction and survey
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• On theories with a combinatorial definition of 'equivalence'
• Nominal Equational Logic
• Capture-Avoiding Substitution as a Nominal Algebra
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Metamathematics, Machines and Gödel's Proof
• Unification of higher-order patterns in linear time and space
• FreshML
• OCaml + XDuce
• Term Rewriting and Applications
• Nominal Unification from a Higher-Order Perspective

This page was built for publication: Matching and alpha-equivalence check for nominal terms