Types and Programming Languages
Types and Programming Languages is a
Level 10 course given in Semester 2, aimed at
4th year
students.
Check the
ITO course descriptor
for the syllabus.
Lectures
Lectures are held on Mondays and Thursdays 3.00-3.50pm in
Appleton Tower room M2A, on the mezzanine level
(nb: note new room, class was formerly in 18 BP 3.15).
Most lectures use Benjamin Pierce's course notes, available
here.
- Mon 7 Jan. The Curry-Howard Isomorphism:
As Natural as 0, 1, 2
(The Curry-Howard Isomorphism)
- Thu 10 Jan. Untyped arithmetic expressions: TAPL, Chapters 1--4. [Lecturer: Sam Lindley]
09/18
09/20
- Mon 14 Jan. Continuing Thu 10 Jan. [Lecturer: Sam Lindley]
- Thu 17 Jan. Untyped lambda calculus: TAPL, Chapters 5--7.
09/25
09/27
10/02
- Mon 21 Jan. Substitution.
10/02
- Thu 24 Jan. Small and big step semantics. Call-by-name and call-by-value.
- Mon 28 Jan. Church booleans, pairs, numerals. Fixpoints.
09/25
- Wed 30 Jan. Simple types. Type rules, reading the rules as an algorithm.
10/02
10/04
10/09
- Mon 4 Feb. Simple types, continued. Progress and Preservation.
- Thu 7 Feb. Implementation issues. (Milner lecture.)
- Mon 11 Feb. Equivalence of small and big step, revisited.
Progress and preservation proofs.
solution to 1.2
10/09
- Thu 14 Feb. Simple extensions to simple types. TAPL, Chapter 11.
10/16
- Mon 18 Feb. Simple extensions to simple types, continued.
- Thu 21 Feb. References, TAPL, Chapter 13. [Lecturer: Sam Lindley]
10/18
- Mon 25 Feb. Exceptions, TAPL, Chapter 14.
10/25
- Thu 28 Feb. Subtyping, TAPL, Chapter 15.
10/30
11/01
- Mon 3 Mar. Subtyping and the Penn interpretation,
TAPL, Chapter 15.
tpl-penn
- Thu 6 Mar. Algorithmic subtyping. TAPL, Chapter 16.
11/13
11/15
- Mon 10 Mar. System F. TAPL, Chapter .
12/04
tpl-church
- Thu 13 Mar. The Girard-Reynolds Isomorphism.
gr
- Mon 17 Mar. Java Generics.
java-generics
java-generics-notes
- Thu 20 Mar. The last lecture.
tpl-final
Exercises
Reading
Most of the course is based closely on
the textbook
Types and Programming Languages
by Benjamin C. Pierce, MIT Press, 2002.
References for other material will be provided as necessary in lectures.
Resources
Here are some other useful resources:
Past instances of the course
Philip Wadler
Last modified: Thu Mar 20 12:13:53 GMT 2008
