January 22, 2015: FWF project “Certification Redux” approved

Christian Sternagel’s project proposal, extending current certification techniques for term rewriting, was approved by the Austrian Science Fund (FWF) in its 51st board meeting. The project has a duration of 3 years and the grant amount is EUR 334K.

In the recent past, certification is very successful in the area of automated termination and confluence proving as well as completion (where certification means the automatic and reliable verification of proofs that were generated by untrusted tools).

The aim of this project is to extend the existing IsaFoR/CeTA project as follows: formalize the recently introduced weighted path order and extend it to rewriting modulo associativity and commutativity (AC-rewriting); support certification of conditional confluence proofs; and formalize the theory of AC-rewriting, AC-unification, and normalized completion. This will bring CeTA up to speed with the most recent tool developments of termination tools (ttt2), confluence tools (csi), and completion tools (mkbtt).