A Coq formalization of an analysis and optimization of While

Grigory Fedyukovich

Institute of Cybernetics

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.

Tarmo Uustalu
Last update 13 November 2009