Foundations of Modern Type Systems

G22.3033.10 Spring 2000

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 01/19 Intro to the simply typed Lambda-calculus Chap. 1, 2.1 - 2.2 (skim), 3.1 - 3.3, 4.1 - 4.3.3 
2 01/26 Types & Logic, proof systems, reduction 4.3.4, 4,3.5, 4.4.1, 4.4.2 
3 02/02  Intro to polymorphism, predicative polymorphism 9.1 - 9.2 
4 02/09  Type inference 11
5 02/16  Impredicative polymorphism, data abstraction  9.3.1-4, 9.4
6 02/23  Effective type inference  
7 03/01  Modules, general products and sums 9.5
8 03/08  The Cube of Type Lambda-Calculi  
03/15 Spring recess
9 03/22 TBD Handout
10 03/29  TBD Handout
11 04/05 Research Issues  Handout 
12 04/12 Research Issues  Handout 
13 04/19 Research Issues  Handout 
14 04/26 Research Issues  Handout 
Final exam

Research issues to be discussed will be determined by student interest. Possibilities include extensions to the ML type system, applications of type inference/verification techniques to non classical static analyses, etc.


[Last change: 02/09/2000]