A polynomial nominal unification algorithm

DOI10.1016/j.tcs.2008.05.012zbMath1154.68108OpenAlexW2024790008MaRDI QIDQ944382

Christophe Calvès, Maribel Fernández

Publication date: 16 September 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.05.012

zbMATH Keywords

graphsunificationnominal syntax\(\alpha \)-equivalencebinders

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05) Graph theory (including graph drawing) in computer science (68R10)

Related Items (15)

Nominal unification with atom-variables ⋮ Unnamed Item ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ Nominal syntax with atom substitutions ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Equivariant unification ⋮ Unnamed Item ⋮ αCheck: A mechanized metatheory model checker ⋮ Nominal AC-matching ⋮ Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Fixed-Point Constraints for Nominal Equational Unification ⋮ Rewriting with generalized nominal unification ⋮ The First-Order Nominal Link ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Nominal unification with letrec and environment-variables

Uses Software

• Freshml

Cites Work

• Unnamed Item
• Unnamed Item
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Implementing Nominal Unification
• Nominal Matching and Alpha-Equivalence
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Unification of higher-order patterns in linear time and space
• Numbering matters
• FreshML
• Typed Lambda Calculi and Applications

This page was built for publication: A polynomial nominal unification algorithm