Computer Laboratory

Course pages 2016–17


  • Lecture notes (including slides).
  • Annotated slides:
  • 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 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.
    • Here is a very recent example of the kind phenomenon discussed in section 3 of the notes - in this case an unsoundness in Java and Scala arising from the combination of ML-style polymorphim with subtype polymorphism: Nada Amin and Ross Tate's Unsound Playground and accompanying paper at OOPSLA 2016.