Name
Abstract | ||
|---|---|---|
This work adapts a formalisation in Coq of a nominal C-unification algorithm to include “protected variables” that cannot be instantiated during the unification process. By introducing protected variables we are able to reuse the C-unification algorithm to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view having this extension would be enough to adapt the C-unification algorithm for dealing with equational check as well as with C-matching problems, but the resulting algorithms would not be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification and reuse previous formalisations. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1016/j.entcs.2019.07.004 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
Nominal Unification,Nominal Matching,Commutative Theory,C-Unification,Formal Methods,Coq | Reuse,Computer science,Unification,Unification process,Theoretical computer science | Journal |
Volume | ISSN | Citations |
344 | 1571-0661 | 0 |
PageRank | References | Authors |
0.34 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| M. Ayala-Rincón | 1 | 10 | 5.38 |
| Washington de Carvalho Segundo | 2 | 0 | 1.69 |
| Maribel Fernández | 3 | 315 | 23.44 |
| Daniele Nantes Sobrinho | 4 | 2 | 3.08 |