Invited talks
Combining tactics, normalization, and SMT solving to verify systems software
Chris Hawblitzel Systems Research Group, Microsoft Research, Redmond, USA
Cocon: A Type Theory for Defining Logics and Proofs
Brigitte Pientka McGill University, Canada