Speaker: Dr. Christian Urban
Time: 3:00pm, 15 Apr. 2011
Abstract :
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.
This is joint work with Chunhan Wu and Xingyuan Zhang from the PLA University of Science and Technology in Nanjing.
Short Bio:
Christian Urban is an Emmy Noether Fellow at the Technical University of Munich (Germany). He received his Ph.D. in 2000 from the University of Cambridge (UK). After his Ph.D., he was awarded a research fellowship at Corpus Christi College in Cambridge. In 2004 he moved back to Germany with the help of a fellowship from the Alexander-von-Humboldt Foundation.
His current research interests include theorem provers, type systems, compilers, formal languages, and semantics of programming languages.
