计算机学院系列报告会之——Dr. Christian Urban

报告人：Dr. Christian Urban

时 间：4月15日下午3:00～4:00

地 点：计算机学院六楼学术报告厅

报告摘要：
Verifying formally the correctness of an algorithm is still fiendishly hard. One way of making such verifications easier is to implement the algorithm directly inside a theorem prover. In the talk I will show how to do this with a simple regular expression matcher. This example will also show that often an algorithm needs to be re-formulated in order to better suit the reasoning in a theorem prover. For example, regular expression matching is normally implemented with finite automata. Unfortunately, automata are a hassle for formalizations in theorem provers, in our case the theorem prover Isabelle/HOL. The reason is that automata need to be represented as graphs or matrices, neither of which can be easily defined as algebraic datatype. In contrast, regular expressions can be defined easily as datatype and a corresponding reasoning infrastructure comes for free. I will show in the second part of the talk that a central result from formal language theory, the Myhill-Nerode theorem, can be recreated using only regular expressions.