Apr 25
(English) Talk by Maribel Fernandez, 26 April
Nominal Completion for Rewrite Systems with Binders
Talk by Maribel Fernandez. Joint work with Albert Rubio.
Venue: Salle de reunion, 10h30 Thursday 26 April 2012
Nominal rewriting generalises first-order rewriting by providing
support for the specification of binding operators, using the
nominal approach. In this talk, I will present a new ordering
that can be used to prove termination of nominal rewriting rules,
generalising the recursive path ordering to take into account
alpha equivalence. Using this ordering, we have designed a
Knuth-Bendix style completion procedure (to our knowledge,
this is the first completion procedure available for rewriting
systems with binders). An implementation can be found at
Nominal Completion for Rewrite Systems with Binders
Talk by Maribel Fernandez. Joint work with Albert Rubio.
Venue: Salle de reunion, 10h30 Thursday 26 April 2012
Nominal rewriting generalises first-order rewriting by providing
support for the specification of binding operators, using the
nominal approach. In this talk, I will present a new ordering
that can be used to prove termination of nominal rewriting rules,
generalising the recursive path ordering to take into account
alpha equivalence. Using this ordering, we have designed a
Knuth-Bendix style completion procedure (to our knowledge,
this is the first completion procedure available for rewriting
systems with binders). An implementation can be found at
