Logic, Specification and Verification

LECTURES: Dr James McKinna and Dr. Stephane Lengrand
TUTORIALS, Question sheets and marking: Dr. Stephane Lengrand
PRACTICALS, Question sheets and marking: Dr. James McKinna


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)