[5-26]On the Correctness of Programming Languages

Date:2009-05-24

Title：On the Correctness of Programming Languages
Speaker：Christian Urban 

          Institute for Computer Science at the TU Munich (IV), Germany.

Time：3:00pm, May 26 
Venue: Lecture room, State Key Lab of Computer Science, Level 3 Building #5


Abstract：
Programming languages have the potential to be distributed widely and if they contain errors it is often difficult to retract them. Consequently, one has to get them right from the beginning. In the talk I will show how theorem provers can help with ensuring the correctness of programming languages and compilers. For this I will discuss empirical evidence we gained with the theorem prover Isabelle, and if time permits I will show how to set up and prove a compiler correctness theorem for a simple WHILE anguage.


About the Speaker：
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). He was a post-doctoral research fellow at Corpus Christi College in Cambridge from 2000-2004, and moved to Germany in 2004 with the help of a fellowship from the Alexander-von-Humboldt Foundation. His current interests include theorem provers, type systems, compilers and semantics of programming languages.