University Homepage School Homepage School Contacts School Search

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 at 10am in JCMB 3315.

• Mon 8 Jan. The Curry-Howard Isomorphism: As Natural as 0, 1, 2.
• Thu 11 Jan. Continuing Mon 8 Jan.
• Mon 15 Jan. Untyped arithmetic expressions: TAPL, Chapters 1--4.
• Thu 18 Jan. No lecture.
• Mon 22 Jan. Untyped lambda calculus: TAPL, Chapters 5--7.
• Thu 25 Jan. Simply typed lambda calculus: TAPL, Chapters 8--10.
• Mon 29 Jan. Extensions to simply typed lambda calculus: TAPL, Chapter 11. [Lecturer: Sam Lindley]
• Thu 1 Feb. References: TAPL, Chapter 13. [Lecturer: Sam Lindley]
• Mon 5 Feb. Exceptions: TAPL, Chapter 14.
• Thu 8 Feb. Normalization: TAPL, Chapter 12.
• Mon 12 Feb. Subtyping: TAPL, Chapter 15.
• Thu 15 Feb. Subtyping: TAPL, Chapter 15. [Lecturer: Sam Lindley]
• Mon 19 Feb. Featherweight Java: TAPL, Chapter 19.
• Thu 23 Feb. Featherweight Java: TAPL, Chapter 19.
• Mon 26 Feb. Featherweight Java: TAPL, Chapter 19.
  Paper: Featherweight Java.
  Examples: feath1.java feath2.java feath3.java feath4.java.
• Thu 1 Mar. Polymorphic lambda calculus: TAPL, Chapter 24.
• Mon 5 Mar. Existential types: TAPL, Chapter 25.
• Thu 8 Mar. Parametricity.
  Paper The Girard-Reynolds Isomorphism.
• Mon 12 Mar. Parametricity, continued.
• Thu 15 Mar. Coercion semantics for subtyping. TAPL, Chapter 15.6.
  Lecture notes
  Paper Inheritance and explicit coercion
• Mon 19 Mar. Review.
  Lecture notes
• Thu 22 Mar. Review.

Most lectures use Benjamin Pierce's course notes, available here.

Exercises

Some exercises are based around OCaml implementations of the type systems studied.

The starting points for these implementations are given by the checkers described in TAPL, available for download.

• Exercise 1
  Issued: Monday 29 January 2007. Due: Monday 19 February 2007.
• Exercise 2
  Issued: Monday 5 March 2007. Due: Monday 19 March 2007. (Due date changed to: 10.00am Thursday 22 March 2007.)
  
  • TAPL, exercises 23.4.3-9, 23.4.11-12.
  • Specimen questions.
  • Final exam, 2004/5.
  • Final exam, 2005/6.

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:

• Other courses based on TAPL, at Pennsylvania, Lausanne, Glasgow.
• Luca Cardelli. Type Systems.
  Handbook article from CRC Handbook of Computer Science and Engineering.
• Lambda the Ultimate programming languages weblog.

Past instances of the course

• 2004/5
  • Practical 1
  • Practical 1 hints
  • Practical 2
• 2005/6
  • Practical 1
  • Practical 2

Exam

The exam paper will contain three questions of which you should answer two. The time allowed will be 1hr45 minutes.

• Here are two specimen questions.
• See the ITO pages for past papers.

Philip Wadler

Last modified: Mon Mar 5 11:06:33 GMT 2007