Loading...
Loading...

Go to the content (press return)

Nominal completion for rewrite systems with binders

Author
Fernandez, M.; Rubio, A.
Type of activity
Presentation of work at congresses
Name of edition
39th International Colloquium on Automata, Languages and Programming
Date of publication
2012
Presentation's date
2012-07-09
Book of congress proceedings
Automata, Languages, and Programming: 39th International Colloquium, ICALP 2012: Warwick, UK, July 9-13, 2012: proceedings, part II
First page
201
Last page
213
Publisher
Springer
DOI
https://doi.org/10.1007/978-3-642-31585-5_21 Open in new window
Project funding
Sweetlogics-UPC
Repository
http://hdl.handle.net/2117/24004 Open in new window
URL
http://link.springer.com/content/pdf/10.1007%2F978-3-642-31585-5_21 Open in new window
Abstract
We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. Completion of rewriting systems with binders is a notably difficult problem; the completion procedure presented in this paper is the first to deal with binders in rewrite rules. We design a completion procedure for nominal...
Citation
Fernández, M.; Rubio, A. Nominal completion for rewrite systems with binders. A: International Colloquium on Automata, Languages and Programming. "Automata, Languages, and Programming: 39th International Colloquium, ICALP 2012: Warwick, UK, July 9-13, 2012: proceedings, part II". Warwick: Springer, 2012, p. 201-213.
Keywords
Completion, Nominal syntax, Orderings, Rewriting
Group of research
LOGPROG - Logic and Programming

Participants