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)