Computer Laboratory

Course material 2010–11

Categorical Logic

Principal lecturer: Dr Sam Staton
Taken by: MPhil ACS


Online resources

I have recommended some texts in the syllabus. Here are some additional links:


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 assessed Agda exercises.
  • 75% of the marks will be given for a take-home exam.