Foundations of Modern Type Systems
G22.3033.03 Fall 1997

Syllabus

This is an extremely approximate schedule of topics to be covered, subject to change at any time. The reading is from Mitchell, Foundations for Programming Languages, unless noted otherwise. Much of the course will be spent following the road map for a type theory course given on page xix of Mitchell.

Class Date Topic Reading
1 9/8 Intro to the simply typed Lambda-calculus Chap. 1, 2.1 - 2.2 (skim), 3.1 - 3.3, 4.1 - 4.3.3
2 9/15 Types & Logic, proof systems, reduction 4.3.4, 4,3.5, 4.4.1, 4.4.2
3 9/22 Intro to polymorphism, predicative polymorphism 9.1 - 9.2
4 9/29 Impredicative polymorphism 9.3.1 - 9.3.4,
5 10/6 Data abstraction and existential types, modules 9.4, 9.5
6 10/13 Subtyping 10.1 - 10.4
7 10/20 Subtyping, cont.
8 10/27 Records as objects, subtyping and polymorphism 10.5, 10.6
9 11/3 Type inference Chap. 11
10 11/10 Type inference, cont.
11 11/17 Research Issues Handout
12 11/24 Research Issues Handout
13 12/1 Research Issues Handout
14 12/8 Research Issues Handout

Research issues to be discussed will be determined by student interest. Possibilities include proposed extensions to the ML module system, the Haskell class system, new OOP type systems, etc.