Computer Aided Formal Reasoning (G5BCFR) - Autumn 2005

Convenor

Tutors

• James Chapman
• Robert Reitmeier

Friends

• Conor McBride
• Peter Morris
• Wouter Swierstra

Content

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.

Software

Assessment

Lectures

• introductory slides from 3/10
• Epigram code from 10/10/05, introducing the propositions as types principle, we define basic propositional connectives (And,Or) and prove simple tautologies.
• Epigram code from 17/10/05, predicates, all, Bool, equality
• Epigram code from 24/10/05, exists, decide equality of Bool, Nat, rec
• Epigram code from 31/10/05, Nat,add,mult,exp,ack,addCom,eqn
• Epigram code from 7/11/05, Decidability of = for Nat, Lists, append, rev, revrev (unfinished)
• Epigram code from 14/11/05,revrev (finished), hd for Lists and Vectors, Fin, vnth
• Epigram code from 21/11/05,vrev with equality proof, definition of Le, show that Le is an equivalence relation and decidable.
• Epigram code from 28/11/05 from an untyped language (Tm) with runtime errors (eval) to a typed langauge with no runtime errors (Eval) and a certified type checker (tcheck)

Coursework

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