Rewriting: Theory and Applications
- LecturerMr. Jiaxiang Liu (Department of Computer Science & Technology, Tsinghua University, China and Laboratoire d'Informatique, École Polytechnique, France)
Host: Bo-Yaw Wang - Time2017-06-21 (Wed.) 10:00 ~ 12:00
- LocationAuditorium 107 at IIS new Building
Abstract
Formal methods are increasingly used for developing critical software. Proof assistants based on type theories allow to formally prove properties of software, in particular, correctness. In expressive type theories allowing for dependent types, computations based on rewriting play a fundamental role in identifying types up to computation, such as
even(2+2) and even(4) which both compute to even(4). This is possible thanks to two crucial properties of rewrite rules, termination and confluence. Confluence is the property of rewriting-based computations expressing that the associated extensional relation is functional, implying uniqueness of normal forms, which exist thanks to termination.
Decreasing diagrams method introduced by van Oostrom is a powerful modern technique for proving confluence. In this talk, we describe this technique and show how we apply it to solve some challenging confluence problems in presence of non-terminating and non-left-linear rules.
Moreover, rewrite systems can serve directly as a modeling tool for system verification. We also show in this talk its application in termination provers for C-programs.