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

graphsnominal syntaxunification\(\alpha \)-equivalencebinders

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

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

Cited in

(32)

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

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)