Program Semantics, Verification, and Construction

(Previous instance: 2007/2008)

2008/2009

Course coordinator: Nelma Moreira (nam(AT)ncc(DOT)up(DOT)pt)

Lecture 1

Lambda Calculus

Date:

07/10/08

Notes:

* Lcalc.pdf

Lecture 2

Deduction Systems and Intuitionism

Date:

13/10/08

Notes:

* psvc02.pdf

Lecture 3

Type systems and the Curry-Howard isomorphism

Date:

21/10/08 (tuesday, 15h-18h)

Notes:

• Simple Types

• Curry-Howard Iso.

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

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

Lecture 4

Operational Semantics

Bibliography:

Semantics with Applications, H. Nielson and F. Nielson. (online version)

Date:

27/10/08 (Monday, 10h-13h) Sala 1

Lecture 5

Denotational Semantics

Date:

03/11/08 (Monday, 10h-13h) Sala 1

Bibliography:

Semantics with Applications, H. Nielson and F. Nielson. (online version)

Lecture 6

Proof assistants based on type theory

Date:

11/11/08 (tuesday, 15h-18h) Sala 1

Notes:

• Type Systems and Logics (01-20) (21-30) (31-61)

Lecture 7

Extensions of Pure Type Systems

The Coq proof assistant

Date:

17/11/08 (Monday, 10h-13h) Sala 1

Notes:

• Beyond Pure Type Systems (01-20) (21-40)

• A Pratical Approach to the Coq System (Slides)(Proof script)(Exercises)

Material:

• Coq web page
• Coq Tutorial
• Coq in a Hurry - a tutorial by Yves Bertot (INRIA, Sophia-Antipolis)
• Coq-Lab - a pratical approach to Coq with exercises, by J-C Filliâtre and C. Paulin-Mohring.

Lecture 8

Functional Program Verification in Coq

Date:

24/11/08 (Monday, 10h-13h) Sala 1

Notes:

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

Lecture 9

Hoare logic and interface specification languages

Date:

15/12/00 (Monday, 10h-13h) Sala 1

Slides:

(see next lecture)

Lecture 10

Verification conditions and program verification in practice

Date:

5/01/09 (Monday, 10h-13h) Sala 1

Slides

Lecture 11

Introduction to the mathematics of program construction

Date:

12/01/09 (Monday, 10h-13h) Sala 1

Topics:Overview of the scientific method applied to software design.Correct by verification versus correct by construction. Calculate versus invent & verify.The e=m+c equation: description versus calculation. Point-free (PF) and point-wise (PW) notations. PF-transform for (algebraic) reasoning.

Analogy with the Laplace transform (historical perspective). Binary relations as a building block for logic in computer science. Introduction to the binary relation calculus.

Notes:

• Theory and applications of the PF-transform Lectures 1-2 (01-56) (slides of the LerNET? doctoral school at Piriapolis, Uruguay, 2008)
• Full tutorial paper: (LNCS)

Lecture 12

PF-transform: when everything becomes a relation

Date:

19/01/09 (Monday, 10h-13h) Sala 1

Topics:

Taxonomy of binary relations. Functions. Conditions and coreflexives. PF-transform of n-ary relations. Products and Sums. Universal constructions and properties. Extended static checking (ESC) in the PF-style. Induction-free calculation of preconditions and invariants. Three case studies.

Notes:

• Theory and applications of the PF-transform Lectures 2-4 (57-124)

Lecture 13

Constructive proofs and program calculation

Date:

26/01/09 (Monday, 10h-13h) Sala 1

Topics:

A PF-approach to polymorphic type checking. Reynolds' relation on functions. The free-theorem of polymorphic functions in one equation. Inductive predicates and relations. The catamorphism concept. Universal property and its corollaries. Mutual recursion. Calculation of for/while loops from systems of mutually recursive equations over linear types.

Notes:

• Theorems for free: a (calculational) introduction (slides)

• Relational algebra: a Kleene algebra central to the mathematics of program construction (slides)