Teaching
Lectures
- Object-oriented software development (2014, 2015). I have given eight-week lecture courses on Java to the keen first-year IT students at Chalmers.
- Functional Programming: Implementation, Specification and Verification (2013). I lectured a new MPhil course for Michaelmas term 2013. This course taught functional programming, the basics of implementing functional programming languages, their formal specification and formal verification of their runtimes and compilers. The course was 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.
Supervision of Bachelors and Masters projects
I have supervised several student projects for topics such as compiler optimisations, verification of compiler optimisations (e.g. register allocation, function-call optimisation), semantics of programming languages (lazy vs strict), and proof automation (for code generation).
Classes and supervisions of small groups
- 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.