Computer Laboratory

Course pages 2011–12

Category Theory and Logic

The course will be assessed by a take-home exam (75%) and by an assessed exercise in the Agda programming language / proof assistant (25%). I will give you exercise sheets which are not assessed but which help you to prepare for the exam.


  • Assessed exercise in Agda: The deadline is midnight on Sunday 27 November 2011.
  • Take-home exam: to be arranged.

Take-home exam

Details coming soon.

Agda assessed exercises

The Agda assessed exercise is here: [exam2011.agda].

The deadline is midnight on Sunday 27 November 2011. Please submit your answers by email to me and also submit a paper copy to student admin in the usual way.

I hope the script is self-explanatory. Let me know if anything is unclear, because others might also be wondering. I'm very happy to answer any questions about Agda.

The first 15 questions (test1 -- test15) just make use of the type theory that we have covered in lectures. They should be easy if you have done any functional programming before.

The remaining 10 marks involve a kind of implementation of type theory inside Agda itself. I've done all the questions myself. I don't think they are too hard, but they are harder than the first 15. I think you are all capable of all the questions.

Guidelines and rules:

  • The best way to interact with Agda is via the Emacs editor. Just open the .agda file inside Emacs. You can then access Agda via the Agda menu or via keyboard shortcuts.
  • We discussed the specifics of Agda in lecture 5 and lecture 9. Everyone learns languages in different ways. Perhaps you prefer to get stuck in, or perhaps you'd rather start by going through one of the tutorials suggested on the materials page.
  • Sometimes Agda will not fail outright but it will still be "concerned" about your program. It indicates this by highlighting the syntax in yellow or salmon. Your final submission should not have any of this highlighting. I have explained this in the file [colours.agda].
  • You are not allowed to collaborate on this exercise because it is assessed. You can discuss Agda with each other, and with me, and I hope you will. Just don't discuss the exercises themselves.
  • In your submission, include any test cases, helper functions, strange variable names... anything to make your own code unique.