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 | Research Issues | Handout |
| 10 | 03/29 | Research Issues | 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]