Program Semantics, Verification, and Construction

2007/2008

---

Lecture 1

Date:

15/10/07

Notes:

• psvc.pdf

Lecture 2

Date:

22/10/07

Topics:

Deduction systems. Natural deduction. Sequent Calculus. Intuitionism.

Notes:

• psvc02.pdf

Reading Material:

• gallier91constructive.pdf: Constructive Logics: part 1 , J. Gallier

• lectures-on-the-curry.pdf: Lectures on Curry-Howard Isomorphism

Lecture 3

Date:

29/10/07

Notes:

• psvc.pdf

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:

• 2 slides by page: (1-20) (21-40) (41-60)

• 4 slides by page: (1-20) (21-40) (41-60)

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:

• Beyond Pure Type Systems (2 up: 1-20, 21-40) (4 up: 1-20, 21-40)
• A Pratical Approach to the Coq System (Slides)(Proof script)(Exercises)

Material:

• Coq web page
• Software (local copy)
• Documentation (local copy)
  • Tutorial (HTML) (PDF)
  • Reference Manual (HTML) (PDF)
  • Standard Library Reference (HTML)

Lecture 8

Date: 03/12/07

Topics: (Functional Program Verification in the Coq System)

Notes:

• Program Verification in Coq (Slides)(Proof script)

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:

• Slides

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:

• Caduceus-examples_MAPi-psvc.zip

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:

• Slides

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:

• Slides

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:

• Slides

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.