• Advanced Object Oriented Programming Languages

We develop formal models for the semantics of Object Oriented Programming Languages. We discuss implementation issues for C++, the Java verifier, dynamic linking and loading, ownership types and their uses.

• Reasoning about Programs

Reasoning about functional programs (induction), and imperative programs (a simplified version of Hoare Logic). Also, well-founded induction, and induction over any inductively defined structure.

Will Sonnex and I developed teaching material using Dafny to support the development of inductive proofs, the expression and testing of lemmas, program specification, and reasoning about imperative programs.  I can supply this material to teachers upon request. The development of the Dafny material was funded by Microsoft Research, organised by Judith Bishop, and supported by Rustan Leino. A video can be found here. A summary available here.

Rustan Leino taught a 3 day min-course on Dafny in March 2014 at Imperial. More details here.