Logic, Specification and Verification 2007

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)