Rewriting: Theory and Applications
- 講者劉嘉祥 先生 (北京清華大學計算機科學與技術系、巴黎綜合理工學院計算機科學實驗室)
邀請人：王柏堯 - 時間2017-06-21 (Wed.) 10:00 ~ 12:00
- 地點資訊所新館107演講廳
摘要
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.