Tuesday, 8 December 2009, 14:00 (note the unusual weekday!)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: I present ongoing work with Keiko Nakata and Tarmo Uustalu to formalize analyses and optimizations for the While language with the Coq proof assistant. I use Coq's feature of inductive definitions to formalize the syntax, semantics and Hoare logic of While. I then develop type systems for live variables analysis and dead code elimination and soundness proofs of these type systems against a relational interpretation of types, following the exposition of Tarmo Uustalu and Ando Saabas.