Types and Programming Languages
- Monday 11.00 Boyd Orr LT B (until 30th October), then F121,
17 Lilybank Gardens
- Wednesday 9.00 2 University Gardens (209)
- Friday 10.00 Maths 214
In most weeks, one of the lecture
sessions (usually Friday) will be used for a tutorial.
Copies of the lecture slides will be distributed during
lectures. Lecture slideshows will be available from this page
after lectures. You should get a copy of the course textbook:
Types and Programming Languages by Benjamin
Pierce. At the end of most lectures there will be a list of
supplementary reading and exercises from Pierce; these exercises
will be discussed during tutorials. Additional exercise sheets
will also be handed out. As a rule (in any course)
you should expect to spend at least as much time on private
study as you spend in classes. Although the material in the
lecture slides is adequate for the course, the more
of the supplementary reading and exercises you do, the better
will be your understanding of the course material.
The SableCC tool.
The Simple Expression Language (SEL) typechecker and accompanying
The Simple Functional Language (SFL) typechecker and accompanying
The Better Functional Language (BFL) typechecker and accompanying
The Functional Language with Sessions (FLS) typechecker.
Here is the assessed exercise. The deadline
is Friday 2nd December.
Here is a week-by-week schedule of topics, with links to worksheets
and other handouts. It will be updated during the term.
The paper Type Systems by
is an excellent survey of many topics that we will cover during the
course. If you are an MSc or MSci student, note that it
is one of the papers that we will be studying in the Research
Readings module (Programming Languages section).
Week 1 beginning 25th September
Week 2 beginning 2nd October
- Monday 2nd: Lecture 1. Introduction to types in
programming languages. Slideshow PowerPoint
Further reading: Pierce Chapter 1.
- Wednesday 4th: Lecture 2. The Simple Expression Language (SEL)
its operational semantics. Slideshow
Further reading: Pierce 3.1, 3.2, 3.4, 3.5; Cardelli (Sections 1 and
2); Ennals, Sharp and Mycroft (Sections 1 and 2).
- Friday 6th: Tutorial (Exercises 1)
- Exercises 1 and solutions.
Pierce 3.5.10, 3.5.18.
- Preliminary reading for next week: Pierce Chapter 8.
Week 3 beginning 9th October
- Monday 9th: Lecture 3. Types and program correctness in
SEL; proving that types guarantee safety.
reading: Pierce 3.3.
- Wednesday 11th: Lecture 4. The Simple Functional Language
reading: Pierce Chapter 8; Ennals, Sharp and Mycroft (Section 2).
- Friday 13th: Tutorial (Exercises 2).
- Exercises 2 and solutions.
Pierce 3.2.4, 3.2.5, 3.5.5, 3.5.13, 3.5.14, 3.5.16, 3.5.17,
8.2.3, 8.3.4, 8.3.5, 8.3.6, 8.3.7, 8.3.8.
Week 4 beginning 16th October
- Monday 16th: Lecture 5. Implementing typecheckers for SEL
Programming Language Processors in Java (David
Watt and Deryck Brown), Chapter 5.
- Wednesday 18th: Lecture 6. Lambda calculus as a
foundation for general functions. Slideshow. PowerPoint
Further reading: Pierce Chapter 5.
- Friday 20th: Tutorial (Exercises
3 and discussion of Ennals, Sharp and
- Exercises 3
- Further exercises: Pierce 5.2.1, 5.3.3, 5.3.7, 5.3.8
Week 5 beginning 23rd October
- Monday 23rd: Lecture 7. Typed lambda calculus and the
Better Functional Language (BFL). Slideshow. PowerPoint
Further reading: Pierce Chapters 9 and 12.
- Wednesday 25th: Lecture 8. Products, records and sums.
Further reading: Pierce Chapter 11.
- Friday 27th: Tutorial (Exercises 4 questions 1-4).
- Exercises 4
Further exercises: Pierce 9.2.1, 9.2.2, 9.2.3, 9.3.9, 9.3.10, 9.4.10,
11.5.2, 11.9.1, 11.11.1, 11.11.2
Week 6 beginning 30th October
- Monday 30th: Lecture 9. References. Slideshow. PowerPoint
Further reading: Pierce Chapter 13.
- Wednesday 1st: Lecture 10. Subtyping; objects.
Further reading: the rest of the handout; Pierce 15.1-15.5, 18.1-18.7.
- Friday 27th: Tutorial (Exercises 4 question 5).
- Exercises 4
Further exercises: Pierce 13.1.1, 13.1.2, 13.4.1, 13.5.2, 13.5.8, 15.2.1, 15.2.5, 15.5.2, 15.5.3.
Week 7 beginning 6th November
- Monday 6th: Lecture 11. Linear types. Slideshow. PowerPoint
Further reading: B. C. Pierce, Advanced Topics in Types and
Programming Languages, Chapter 1.
- Wednesday 8th: Lecture 12. Linear types, continued.
Further reading: "Linear Types for Packet Processing", Section 3;
- Friday 10th: Tutorial (any questions; packet processing).
Week 8 beginning 13th November
Week 9 beginning 20th November
Week 10 beginning 27th November
- Monday 27th: Lecture 17. Pi calculus.
- Wednesday 29th: Lecture 18. Types in pi calculus.
- Friday 1st: Tutorial (Exercises 5).
- Exercises 5