- 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.