Course pages 2014–15
Types
- Lecture notes (including slides)
- Slides from the lectures (contains additional notes/examples):
- Lecture 1
- Lecture 2
- Lecture 3
- Lecture 4
- Lecture 5
- Lecture 6
- Lecture 7
Code from the lecture (plus some extra):- Tautology.agda - example of a tautology checker using dependent function types in Agda
- List.agda - demonstration of the PLC representation for the list ADT (in Agda)
- Tree.agda (not shown in lecture) - demonstration of the PLC representation for a leaf-labelled tree ADT
- Lecture 8
- Exercise sheet
- Additional material:
- Naive implementations of the ML type inference algorithm (Section 2.4) and the PLC type inference algorithm (Section 4.3). Both are written in Fresh O'Caml, which is a patch of O'Caml with very cool facilities for handling binding and freshness of names.
- Need more help understanding the material in Section 3 (Polymorphic Reference Types)? Try 1.1.2.1 Value Polymorphism of the "SML'97 Conversion Guide" provided by SML/NJ.
- The types forum carries discussion and announcements concerning research into type systems.