Teaching
Lectures
- Functional Programming: Implementation, Specification and Verification (2013). I'm currently lecturing a new MPhil course for Michaelmas term 2013. This course teaches functional programming, the basics of implementing functional programming languages, their formal specification and formal verification of their runtimes and compilers. The course is partly based on my research on verified implementations of Lisp and ML.
- Hoare Logic (2012). When Prof. Mike Gordon was on sabbatical in the academic year 2012-2013, I lectured, set and marked exam papers for this course which teaches Hoare Logic and introduces Separation Logic to final-year undergraduates.
- Foundations of Computer Science (2010). When Prof. Larry Paulson was on sabbatical in the academic year 2010-2011, I lectured, set and marked exam papers for this course on the theoretical concept underlying computer science. This course was aimed at first-year undergraduates.
Classes and supervisions
- Specification and Verification I. I've given two-hour classes for final-year undergraduates in this verification course.
- Optimising Compilers, Temporal Logic, Discrete Maths and Hoare Logic. I've supervised, in small groups, undergraduates for these courses.