LECTURES: Dr James McKinna and Dr. Stephane Lengrand
TUTORIALS, Question sheets and marking: Dr. Stephane Lengrand
PRACTICALS, Question sheets and marking: Dr. James McKinna
LECTURES
|
TUTORIALS
Coq library developed for these tutorials CS3202.v
|
06/02/2007, Lecture 0: Module Overview
Slides .pdf
|
06/02/2007, Lecture 1: Review of logic, syntax and semantics
Slides .pdf
|
12/02/2007, Lecture 2: Propositional logic - The notion of proof in
Natural Deduction
Slides .pdf
|
13/02/2007, Lecture 3: Writing down proof-trees (Dr. James McKinna)
|
13/02/2007, Tutorial 1 .pdf
Template CS3202tutorial1.v
Correction CS3202tutorial1C.v
(20/02/2007)
|
20/02/2007, Lecture 4: Intuitionistic vs. classical logic -
Decorating proof-trees with variables and terms
Slides .pdf
|
26-27/02/2007, Lecture 5: Predicate Logic .pdf
|
02/03/2007, Lecture 6: Predicate Logic -
Semantical notions, equality & conclusion
Slides .pdf
|
06/03/2007, Tutorial 2 .pdf
Template CS3202tutorial2.v
Correction CS3202tutorial2C.v
(09/03/2007)
|
12/03/2007, Lecture 7: Induction
Slides .pdf
Example of a proof by induction: commutativity of addition Induction.v
|
20/03/2007, Lecture 8: Lambda-calculus (Dr. James McKinna)
|
14/04/2007, Demonstration: Insert Sort, or how to extract the program from
the proof Insert_Sort.v
|
10/04/2007, Lecture 9: From Lambda-calculus to Coq (Dr. James McKinna)
|
17/04/2007, Tutorial 3 .pdf
Correction CS3202tutorial3C.v
(23/04/2007)
|