A polynomial nominal unification algorithm

DOI10.1016/J.TCS.2008.05.012MaRDI QIDQ944382zbMATH OpenOpenAlexFDO

Authors 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

\(\alpha \)-equivalencebindersgraphsnominal syntaxunification

Mathematics Subject Classification ID

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

Recommendations

• An efficient nominal unification algorithm
• Implementing nominal unification
• Term Rewriting and Applications
• Nominal unification
• Equivariant unification

Cites work

• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• FreshML: programming with binders made simple
• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 1437942 (Why is no real title available?)
• Implementing nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal Matching and Alpha-Equivalence
• Nominal rewriting
• Nominal unification
• Numbering matters
• Typed Lambda Calculi and Applications
• Unification of higher-order patterns in linear time and space

Cited in

(33)

• Nominal unification with atom-variables
• On solving nominal fixpoint equations
• Unification of hypergraph \(\lambda\)-terms
• Nominal unification
• Nominal unification with letrec and environment-variables
• Nominal syntax with atom substitutions: matching, unification, rewriting
• Nominal unification of higher order expressions with recursive let
• Nominal syntax with atom substitutions
• Implementing nominal unification
• Unifying nominal unification
• The First-Order Nominal Link
• Constraint solving in non-permutative nominal abstract syntax
• Nominal Matching and Alpha-Equivalence
• Unity in nominal equational reasoning: the algebra of equality on nominal sets
• αCheck: A mechanized metatheory model checker
• Meta-variables as infinite lists in nominal terms unification and rewriting
• Fixed-point constraints for nominal equational unification
• Nominal unification with atom and context variables
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• A certified functional nominal C-unification algorithm
• Rewriting with generalized nominal unification
• On nominal syntax and permutation fixed points
• Nominal anti-unification
• Computer Science Logic
• An efficient nominal unification algorithm
• Automata, Languages and Programming
• Term Rewriting and Applications
• (Nominal) unification by recursive descent with triangular substitutions
• Nominal AC-matching
• Equivariant unification
• Unranked Nominal Unification
• A nominal approach to equational problems in languages with binders
• Matching and alpha-equivalence check for nominal terms

Describes a project that uses

Uses Software

• FreshML

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q944382)