Course pages 2015–16

Types

• Lecture notes (including slides).
• List of corrections to the notes.
• Annotated slides:
  • lecture 1 (13 Oct)
  • lecture 2 (15 Oct)
  • lecture 3 (20 Oct)
  • lecture 4 (22 Oct)
  • lecture 5 (27 Oct)
  • lecture 6 (29 Oct)
  • lecture 7 (3 Nov)
  • lecture 8 (5 Nov)
  • lecture 9 (10 Nov)
  • lecture 10 (12 Nov)
  • lecture 11 (17 Nov)
  • lecture 12 (19 Nov)
• 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 OCaml, which is a patch of OCaml with nice facilities for handling binding and freshness of names.
  • Need more help understanding the material in Section 3 (Polymorphic Reference Types)? Try Section 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.
  • Some interesting examples of dependently typed programming languages:
    • Agda is a both a dependently typed functional programming language with Haskell-like syntax and a proof assistant.
    • Coq is both a proof assistant and a dependently typed functional programming language with an OCaml-like syntax.
    • F* is a verification-oriented dialect of ML.