Implementing nominal unification

DOI10.1016/J.ENTCS.2006.09.027zbMATH Open1278.68118OpenAlexW2102485270MaRDI QIDQ2867897FDOQ2867897

Authors: Christophe Calvès, Maribel Fernández 

Publication date: 20 December 2013

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.09.027

Recommendations

• A polynomial nominal unification algorithm
• An efficient nominal unification algorithm
• Unifying nominal unification
• Automata, Languages and Programming
• Term Rewriting and Applications

zbMATH Keywords

nominal syntaxunificationtermgraphs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Nominal unification
• Unification of higher-order patterns in linear time and space
• Logic Programming
• Numbering matters

Cited In (11)

• Rewriting with generalized nominal unification
• Meta-variables as infinite lists in nominal terms unification and rewriting
• A formalisation of nominal C-matching through unification with protected variables
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• A polynomial nominal unification algorithm
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Title not available (Why is that?)
• Formalising nominal C-unification generalised with protected variables
• Unification of hypergraph \(\lambda\)-terms
• Nominal Matching and Alpha-Equivalence

Uses Software

• Maude
• OCaml

This page was built for publication: Implementing nominal unification

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