DM22, Spring 2007 - Weekly Note 11

Lecture April 16

More on proofs of properties of code. The extensionality principle. Start on type inference.

Reading

Sections 1.4.1 and 4.2-4 in Bird again, now with a focus on proofs. Handouts from Thompson book (Chapter 13, will be handed out next time).

Comments

The author is fond of general laws allowing substitution of one expression (typically involving standard functions) for another. In particular, he likes their use in program derivation, where the starting point is an obviously correct, but inefficient expression, which is then transformed into a more efficient one through a sequence of equivalent expressions (which maintains correctness). For extensive examples of this, see Section 4.6 (not curriculum).

Lecture April 23 (Expected Contents)

More on type inference. Start on Prolog.

Reading

Handouts from Thompson book (Chapter 13).

Exercises April 25

Exam of summer 2005 (pdf), exercise 4.

Exam of winter 2007 (pdf), exercise 4.

Exercises 2.4.1, 2.5.2, 4.3.4, and 4.4.3 in Bird.

(The following exercises should only be attempted after the lecture April 23.)

Exercises 1.6.1, 1.6.3, and 1.6.4 in Bird.

Exam of winter 2000 (pdf), exercise 1, question a.