Computer Aided Formal Reasoning (G5BCFR) - Autumn 2005


Thorsten Altenkirch,




This module introduces the student to computer aided formal reasoning an emerging technology with interesting applications such as proof carrying code or certified safety critical systems. The course includes a practical component by using the EPIGRAM system and a theoretical component providing some background on the theory of formal reasoning.


We will use the Epigram system, a programming and verification language and software development system based on Type Theory, developed by Conor McBride. You find most relevant information about Epigram on the Epigram homepage, e.g. the epigram manual or an epigram tutorial and some background reading such as Why Dependent Types Matter. Epigram is freely available on most platforms, e.g. Linux, MAC OS and Windows. You have to install xemacs first, because Epigram uses xemacs as a user interface. We will install epigram on machines in the lab and make copies available on CD.


The course is assessed by coursework (40%) and a 2 hour online exam (60%). The coursework is mainly based on lab work with the epigram system.



Can be signed off, Tuesdays 1200-1300 in A39 or at another time, if agreed with me or one of the tutors. In any case the coursework has to be completed before the set deadline, otherwise points will be reduced (10% per working day). The successful completion of the coursework will be confirmed by email.

  1. Coursework (10%), set Tuesday 11/10, to be completed Tuesday 25/10, 1300.
    Load ex1.epi into epigram. It contains definitions of the logical connectives And, Or, Not as discussed in the lecture. It also contains 14 empty sheds, [], which you should complete. The succesful completion of a shed is signalled by the background turning green after pressing escape, and the smile on the face of the tutor. You are allowed, in some cases encouraged, to introduce auxilliary definitions (lets) by double clicking on the separators -----.
  2. Coursework (10%), set Tuesday 25/10, to be completed Tuesday 8/11, 1300.
    Load ex2.epi into epigram. There are a number of sheds to be completed. Again, you may need auxilliary definitions. There are some further explanations in comment sheds (those are not supposed to be evaluated).
  3. Coursework (20%), set Tuesday 15/11 to be completed Tuesday 6/12

Thorsten Altenkirch
Last modified: Tue Nov 29 11:59:35 GMT 2005