Teaching and student supervision

I taught the following courses in the Computer Laboratory at the University of Cambridge:

  • “Interactive Theorem Proving in Isabelle/HOL” MPhil/Part III course, covering for Larry Paulson who was away on sabbatical leave, academic year 2017-2018.
  • Model checking component of the “Hoare Logic and Model Checking” Part II course, academic year 2016-2017.
  • Invited lecture: “Super-advanced functional programming, or dependently-typed programming in Agda” for the MPhil/Part III Advanced Functional Programming Course, academic year 2016-2017.

At Cambridge, I also supervised a number of student projects of various types:

  • Bradley Hardy, Part II Cambridge Computer Science Tripos project supervision with Andy Pitts.  Project title: Better equational reasoning for Agda.
  • Michael Rawson, Part II Cambridge Computer Science Tripos project supervision with Vincent Gomes.  Project title: Verified metatheory and type checking for the simply-typed lambda calculus.
  • James Woods, Part II Cambridge Computer Science Tripos project supervision with Matthew Daggitt.  Project title: Formalising a semiring framework for shortest-distance problems.
  • Lauren Pick, Part II Cambridge Computer Science Tripos project supervision with Ali Sezgin and Alan Mycroft.  Project title: Implementing the IC3 model checking algorithm.
  • Swaraj Dash, Part II Cambridge Computer Science Tripos project supervision with Jeremy Yallop.  Project title: Invertible syntax descriptions in Agda.
  • Nikolaos Athanasiou, Cambridge Undergraduate Research Opportunity student, summer 2015.  Project title: Implementing the Constructive Reals in Agda.
  • Swaraj Dash, Cambridge Undergraduate Research Opportunity student, summer 2015.  Project title: Implementing the Constructive Reals in Agda.
  • Leonhard Markert, Part III Cambridge Computer Science Tripos project supervision with Timothy Griffin.  Project title: Big operators in Agda.

Add a Comment

Your email address will not be published. Required fields are marked *