Time
|
Topic
|
Lectures & Readings
|
Assignment
|
Feb. 28
|
Introduction
|
LEC: Overview;
type system introduction;
Prepare: read chap. 1, chap. 2
|
Assignment #1: software install
|
Mar. 7
|
Untyped Arithmetic Expressions
|
LEC:
math foundation;
untyped arithmetic;
Prepare: read chap. 3, chap. 4
Exercise: 3.5.18
|
Assignment #2: arith
|
Mar. 14
|
Untyped lambda-calculus
|
LEC: untyped lambda calculus;
Prepare: read chap. 5, 6, 7
Exercise: 5.3.8, 6.2.2
|
Assignment #3: lambda calculus
|
Mar. 21
|
Recitation
|
Prepare: Official tutorial
PPT: Review 1
|
|
Mar. 28
|
De Bruijn Representation
|
LEC:
De Bruijn Representation;
closure;
|
|
Apr. 10
|
Simple Types
|
LEC: Typed arithmetic expressions;
Simply typed lambda-calculus;
Prepare: read chap. 8, 9, 10
Exercise: 8.3.6, 9.3.9
|
Assignment #4: types
|
Apr. 23
|
Recitation
|
LEC: Review 2;
De Bruijn Representation;
Simple Extensions;
Prepare: read chap. 11
|
|
Apr. 25
|
Reference
|
LEC:
References;
Prepare: read chap. 13, 14
|
Assignment #5: reference
|
May 1
|
No Class
|
Happy Labor Day!
|
|
May. 9
|
No class
|
|
|
May. 16
|
Exception
|
LEC:
Exception;
Prepare: read chap. 15, 16, 17
|
Assignment #6: exceptions
|
May. 23
|
Subtyping and Imperative object
|
LEC: Imperative objects;
Subtyping;
Metatheory for Subtyping;
Prepare: read chap. 18, 19
|
Assignment #7: subtyping
|
May. 30
|
FJ and Recursive types
|
LEC: Recursive types
Featherweight Java;
Prepare: read chap. 20
|
|
June. 6
|
Recitation
|
PPT: Review 3
|
|
June. 13
|
Type Reconstruction
|
LEC: Type reconstruction
Prepare: read chap. 22
|
Assignment #8: Type Reconstruction
|
June. 20
|
Universal types
|
LEC: Universal types
Prepare: read chap. 23
|
Assignment #9: System F
|
TBA
|
Existential types, Higher-order systems
|
LEC:
Existential types and ADT;
Type operators;
Fω
Prepare: read chap. 24, 29, 30
|
Assignment #10: λω and doc
Assignment #11: Fω and
doc
|
TBA
|
Final test
|
Open book, open notes, no electronic devices
|
|