Computer Laboratory > Teaching > Course material 2009–10 > All courses > Categorical Logic


Categorical Logic

Principal lecturer: Dr Samuel Staton
Taken by: MPhil ACS



The Agda language is available here and is already installed on the MPhil machines.

You may like to read these Agda notes by Ulf Norell.

There is also a guide to Unicode input for the Agda emacs mode.

I will put sample source code and exercises in this directory.


  • 25% of the marks for this course will be awarded for completing the Agda exercises. You need to complete these assessed exercises by Friday 12th March.
  • 75% of the marks will be given for a take-home exam which will be set on Tuesday 27th April. You will have a week to complete it.