Speaker: Adam Koprowski (OAS, TU/e)
Title: Termination of Term Rewriting Meets Theorem Proving

Abstract:
  For few years the emphasis in the research area of termination
of term rewriting is on automation. Since 2004 the annual
termination competition is being held, that stimulates development
of tools for proving termination. Every year the tools and the
proofs generated by them get more involved. The former means that
the tools, inevitably, will (and do) contain some bugs. The latter
means that the generated proofs are more and more difficult to
verify by hand.

  This was the motivation for the CoLoR project, started by
Frederic Blanqui. CoLoR stands for Coq Library on Rewriting and
Termination and, as the name suggests, its goal is to provide a
library of theoretical results concerning termination of term
rewriting, verified in the Coq theorem prover. It is accompanied by
Rainbow: a mechanism aiming at translating, with the help of CoLoR,
termination proofs generated by the tools into complete Coq proofs
certifying termination.

  In this talk I will try to give an overview of the present
status of the works on certification of termination of term
rewriting. I will also zoom-in into the recent contribution in this
field: formalization of matrix interpretations.