Types and Programming Languages

Lecture Times

• 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.

Implementations

The SableCC tool.

The Simple Expression Language (SEL) typechecker and accompanying notes.

The Simple Functional Language (SFL) typechecker and accompanying notes.

The Better Functional Language (BFL) typechecker and accompanying notes.

The Functional Language with Sessions (FLS) typechecker.

Assessed Exercise

Course Material

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 Luca Cardelli 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

• NO LECTURES

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) and its operational semantics. Slideshow PowerPoint
  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.
  Further exercises: 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. Slideshow PowerPoint
  Further reading: Pierce 3.3.
• Wednesday 11th: Lecture 4. The Simple Functional Language (SFL). Slideshow PowerPoint
  Further reading: Pierce Chapter 8; Ennals, Sharp and Mycroft (Section 2).
• Friday 13th: Tutorial (Exercises 2).
• Exercises 2 and solutions.
  Further exercises: 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 and SFL. Slideshow PowerPoint
  Further reading: 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 Mycroft).
  
• 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. Slideshow. PowerPoint
  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. Slideshow. PowerPoint
  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. Slideshow. PowerPoint
  Further reading: "Linear Types for Packet Processing", Section 3; additional notes.
• Friday 10th: Tutorial (any questions; packet processing).

Week 8 beginning 13th November

• Monday 13th: Lecture 13. Type reconstruction. Slideshow. PowerPoint
  
• Wednesday 15th: Lecture 14. Type reconstruction, continued; unification. Slideshow. PowerPoint
  Further reading: Pierce Chapter 22.
• Friday 17th: Tutorial (Exercises 6).
• Exercises 6

Week 9 beginning 20th November

• Monday 20th: Lecture 15. Polymorphism. Slideshow. PowerPoint
  
• Wednesday 22nd: Lecture 16. Pi calculus. Slideshow. PowerPoint
• Friday 17th: Tutorial (Exercises 6).
• Exercises 6

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