Program Semantics, Verification, and Construction
2007/2008
Lecture 1
Date:
15/10/07
Notes:
Lecture 2
Date:
22/10/07
Topics:
Deduction systems. Natural deduction. Sequent Calculus. Intuitionism.
Notes:
Reading Material:
Lecture 3
Date:
29/10/07
Notes:
Lecture 6
Date: 19/11/07
Topics: (Type System and Logics)
Proof assistants based on type theory. Pure Type Systems. The Lambda Cube. The Logic Cube.
Notes:
Lecture 7
Date: 26/11/07
Topics: (Beyond Pure Type Systems + A Pratical Approach to the Coq System)
Extensions of Pure Type Systems: Sigma Systems; Inductive Types. The Calculus of Inductive Constructions. Introduction to the Coq proof assistant.
Notes:
Material:
Lecture 8
Date: 03/12/07
Topics: (Functional Program Verification in the Coq System)
Notes:
Lecture 9
Date: 10/12/07
Topics:
The Central Problem of Formal Methods: Model Validation; Program Derivation; Program Verification. Introduction to Hoare Logic. Program Annotation and Automated Static Checking. The ESC/Java2 tool.
Notes:
Lecture 10
Date: 17/12/07
Topics:
Limitations of ESC/Java2: Examples where correctness or completeness fails.
The Caduceus tool for program verification: usage with Coq and Simplify. The Caduceus workflow.
Simple examples proved with automatic tactics. More complex examples. Case reasoning; frame conditions; modular reasoning.
Example programs and proof scripts:
Lecture 11
Date: 07/01/08
Topics:
Introduction to the mathematics of program construction.
Correct by verification versus correct
by construction. Description versus calculation.
Historical perspective on the PF-transform.
Point-free notation and reasoning. Rules of the
PF-transform.
Notes:
Lecture 12
Date: 14/01/08
Topics:
PF-transform: when everything becomes a relation. Introduction to the binary relation
calculus. Taxonomy of binary relations. Functions.
Conditions and
coreflexives. PF-transform of n-ary
relations. Products and Sums. Universal
constructions and properties. Galois connections.
Notes:
Lecture 13
Date: 21/01/08
No lecture (Lecturer away in an international advisory board meeting)
Lecture 14
Date: 28/01/08
Topics:
Constructive proofs. A PF-approach to
polymorphic type checking. Reynolds' relation on
functions. The free-theorem of polymorphism in one
equation. Extended static checking (ESC) in the
PF-style. Induction-free calculation of preconditions
and invariants. Three case studies.
Notes:
Lecture 15
Date: 04/02/08
Topics:
First part (two hours): Assessment0708 (paper presentations).
Second part (one hour): Discussion. Open issues and hot topics in the mathematics of program
construction. Research directions in
correct by construction.