Name
Abstract | ||
|---|---|---|
Nominal unification is an extension of first-order unification that takes into account the \alpha-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixpoint problems, whose solutions can be generated by algebraic techniques on combinatorics of permutations. |
Year | Venue | DocType |
|---|---|---|
2017 | LOPSTR | Conference |
Volume | Citations | PageRank |
abs/1709.05384 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mauricio Ayala-Rincón | 1 | 156 | 31.94 |
| Washington de Carvalho Segundo | 2 | 0 | 1.69 |
| Maribel Fernández | 3 | 0 | 3.72 |
| Daniele Nantes-Sobrinho | 4 | 0 | 1.69 |