Computer Aided Formal Reasoning (G53CFR,G54CFR)

Exam

The exam is going to take place Friday, 4 June 2010, 900 - 1100 in room B52 in the CS building (i.e. the room where the practicals took place). The exam will be entirely Agda based.

If you have any questions about the material or general questions about the exam, please come and see me in my office (A10), Wednesday 2 June, 1330 - 1430.

Course Information

• Lecturer: Thorsten Altenkirch
• Module Code: G53CFR, G54CFR
• Duration: Spring 2010
• Lectures: Tuesday 0900-100, Tuesday 0900 - 1000, Thursday 0900 - 1000 (both: JC-INTHSE-A12) (1st lecture: Tuesday 26/1)
• Practicals: Friday, 10-11, B52 (starting 29/1)

Lecture material

1. Lecture (Tuesday, 26/1) : Introduction
   
   • Slides
   • Wikipedia: Zermelo-Fraenkel set theory, Intuitionistic type theory, Per Martin-Löf
2. Lecture (Thursday, 28/1): A first taste of Agda
   
   • Agda code (for download)
   • How to type in Unicode characters for Agda in emacs.
   • Commands in Agda-mode in emacs
3. Lecture (Tuesday, 2/2) : Error propagation in Agda
   
   • Discussion: Agda vs Haskell
   • Agda code (for download)
4. Lecture (Thursday, 4/2) : Dependent Types
   
   • Agda code (for download)
5. Lecture (Tuesday, 9/2) : Propositional logic
   
   • Agda code (for download)
   • Wikipedia: Curry-Howard correspondence
6. Lecture (Thursday, 11/2) : Classical principles
   
   • Agda code (for download)
   • Wikipedia: Excluded Middle, Proof by contradiction
7. Lecture (Tuesday, 16/2) : Predicate logic
   
   • Agda code (for download)
   • G52MC2 lectures on predicate logic:
     • L04 : Bool and predicate logic
     • L05 : General predicate logic
     • L06 : More predicate logic
8. Lecture (Thursday, 18/2) : The Axiom of Choice
   
   • Whiteboard: A map of Type Theory
   • Finished Predicate Logic (Equality), see Agda code (for download)
   • Agda code (for download)
   • Wikipedia: Axiom of Choice
9. Lecture (Tuesday, 23/2) : Arithmetic and fast reverse
   
   • Agda code (for download)
10. Lecture (Thursday, 25/2) : Equality, induction and recursion and decidability.
    
    • Whiteboard: Equality
    • Agda code (for download)
11. Lecture (Tuesday, 2/3) : Inductive relations.
    
    • Agda code (for download)
12. Lecture (Thursday, 4/3) : Inductive relations.
    
    • Review of last lecture on the whiteboard: less or equal, combinatory logic
13. Lecture (Tuesday, 9/3) : Evaluator and type checker.
    
    • Agda code (for download, w.o. record constructors)
14. Lecture (Thursday, 11/3) : Typed Assembly Language.
    
    • Agda code (for download)
15. Lecture (Tuesday, 16/3) : Coinductive definitions.
    
    • Agda code (for download)
16. Lecture (Thursday, 18/3) : More on coinductive definitions.
    
    • Agda code (for download)
17. Lecture (Tuesday, 23/3) : Merge Sort (I - II) (Peter Morris)
    
    • Agda code (I) (for download)
    • Agda code (II) (for download)
18. Lecture (Thursday, 25/3) : Merge Sort (III). (Peter Morris)
    
    • Agda code (for download)
19. Lecture (Tuesday, 30/3) : Merge Sort (IV) (Peter Morris)
    
    • Agda code (for download)
20. Lecture (Tuesday, 4/5) : Russell's paradox
    
    • Wikipedia: Russell's paradox
    • Agda code (for download)

Online Resources

• The Agda wiki
• The Agda Reference Manual
• The Agda Library
• Agda tutorial

Coursework

Marks so far for g53cfr, g54cfr (cw 1 - 8).