MAP/i - Foundations of Computing

Option I: Program Semantics, Verification, and Construction

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.

r15 - 27 Sep 2008 - 11:43:58 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM