Introduction to Formal Reasoning (G52IFR)
New: Preliminary marks
Please follow the link for the prelimiminary marks for the course. These marks may still change and need to be confirmed by the board of examiners.
Course Information
- Lecturers: Thorsten Altenkirch and Peter Morris
- Tutors:
- Module Code: G52IFR
- Duration: Autumn 2011, Semester 1
- Lectures: Monday, 1600-1800 in JC-EXCHGE-D.LT3
- Practicals: Tuesday, 1600-1800, Computer Science A32 (starting 11/10)
- Tutorials
- Online Forum. Here are archives of old fori: 2010, 2009, 2008
- The Online exam is on Tuesday, 6/12/2011 at 16:00 in A32. The exam lasts for 2 hours and is at the same time and place as the usual lab. Please note that there is no additional exam in the exam period.
- There are no G52IFR lectures on Monday, 28 November.
Lecture material
- Introduction (3/10/)
- Propositional Logic (10/10/) , coq source
- Predicate Logic (17/10/) , coq source
- Bool (24/10/) , coq source
- Making Sets (24/10/) , coq source
- Peano Arithmetic (31/10/) , coq source
- Lists (7/11/) , coq source
- Compiling expressions (14/11/) , coq source
- Coq in Coq (14/11/) , coq source
Lecture notes (so far) as a pdf.
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
Reading
The Coq book: Coq'Art: the Calculus of Inductive Constructions by Yves Bertot, Pierre Casteran.
Copies are available in the library!
Coursework
Course work marksPlagiarism policy: Students will be asked (randomly) to explain their solutions to their tutor, failing to do so may result in the mark being decreased.
- coursework, set 10/10/11, due 18/10/11, 18:00, online submission, id 412 (solution)
- coursework, set 17/10/11, due 1/11/11 (extended), 18:00, online submission, id 413 (solution)
- coursework, set 31/10/11, due 8/11/11, 18:00, online submission, id 417 (solution)
- coursework, set 7/11/11, due 15/11/11, 18:00, online submission, id 425 (solution)
- coursework, set 14/11/11, due 22/11/11, 18:00, online submission, id 432 (solution)
- coursework, set 21/11/11, due 29/11/11, 18:00, online submission, id 437 (solution)