Implementing nominal unification

DOI10.1016/J.ENTCS.2006.09.027MaRDI QIDQ2867897zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

nominal syntaxunificationtermgraphs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

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

Cites work

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

Cited in

(11)

• Meta-variables as infinite lists in nominal terms unification and rewriting
• Rewriting with generalized nominal unification
• 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
• scientific article; zbMATH DE number 522849 (Why is no real title available?)
• Formalising nominal C-unification generalised with protected variables
• Unification of hypergraph \(\lambda\)-terms
• Nominal Matching and Alpha-Equivalence

Describes a project that uses

Uses Software

• OCaml
• Maude

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)