## 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*.