Mathematics for Computer Scientists 2 (G52MC2)

Online Exam

The online (Coq) exam is taking place, Tuesday 1 December, 11:00 - 13:00 (i.e. the usual time of the lecture and the practical) in A32 (the main lab).

No Lecture on 26/11/09

There will be no MC2 lecture on Thursday, 26/11/09.

Course Information

• Lecturer: Thorsten Altenkirch
• Tutors:
  • George Giorgidze
  • Iain Lane
• Module Code: G52MC2
• Duration: Autumn 2009, Semester 1
• Lectures: Tuesday, 1100-1200 in JC-EXCHGE-D.LT3 (exception: 27/10/09 in JC-EXCHGE-C3), Thursday, 1700-1800 in JC-EXCHGE-C.LT2 (1st lecture: Tuesday 29/9)
• Practicals: Tuesday, 1200-1300, A32 (starting 26/9)
• Tutorials: starting 5/10, please follow the link to find out your tutorial allocation, or if you have any queries wrt tutorials.
• Online Forum
• Last year's forum (read only)

Lecture material

• L01: Intro (24/9/09),coq script
• L02: Coq Basics, Propositional Logic (1/10/09),coq script
• L03: More Coq, Classical Logic (8/10/09),coq script
• L04 : Bool and predicate logic (13/10/09, 15/10/09), coq script (updated, 15/10/09)
• L05 : General predicate logic (20/10/09), coq script
• L06 : More predicate logic (22/10/09),coq script
• L07 : Operations on sets (27/10/09, 29/10/09), coq script
• L08 : Peano Arithmetic (3/11/09, 5/11/09), coq script
• L09 : Some algebra (10/11/09), coq script
• L10 : Primitive recursion (12/11/09), coq script
• L11 : The ω-hotel, diagonalisation (17/11/09), coq script
• L12 : Lists (19/11/09), coq script

Online Resources

• The Coq Home Page
• The Coq FAQ
• The Coq library
• The Coq reference manual
• The coq club mailing list
• Cocorico : the Coq wiki

Also, use Google, Wikipedia.

Reading

The Coq book: Coq'Art: the Calculus of Inductive Constructions by Yves Bertot, Pierre Casteran.

The Coq'Art homepage

Copies are available in the library!

Coursework

Coursework marks

We plan to set 8 weekly assignments, but will only count the 5 best submissions for the assessment.

Plagiarism policy: Students may be asked to explain their solutions to their tutor, failing to do so may result in the mark being decreased.

1. coursework, set 1/10/09, due 8/10/09, 17:00, online submission, id 220, solution.
2. coursework, set 8/10/09, due 15/10/09, 17:00, online submission, id 221, solution.
3. coursework, set 15/10/09, due 22/10/09, 17:00, online submission, id 223, solution.
4. coursework, set 22/10/09, due 29/10/09, 17:00, online submission, id 224, solution.
5. coursework, set 29/10/09, due 5/11/09, 17:00, online submission, id 226, solution.
6. coursework, set 5/11/09, due 12/11/09, 17:00, online submission, id 227, solution.
7. coursework, set 12/11/09, due 19/11/09, 17:00, online submission, id 235, solution.
8. coursework, set 19/11/09, due 26/11/09, 17:00, online submission, id 236, solution.