| The first meeting is on Jan 2, 2002 in Cullinane Hall 149 at 4:00pm.
We will discuss the meeting time and basic course administrivia. Please contact me if you miss the first meeting concerning
meeting times, meeting place, and covered material. The course consists of three parts:
- Operational Semantics, the study of a mathematical
specification of a the behavior of all programs;
- Basic Type Systems and Type Soundness, the study of type
systems and their relationship to an operational semantics;
- Advanced Type Systems, the study of type systems for
complex language constructs.
A more detailed syllabus may be provided during the quarter, if I find
the time.
| Week | Book | Topic |
|---|
| Jan 02 | n/a | Introduction
| | Jan 07 | FF I | Inductive Definitions, Inductive Proofs
Reductions, Calculi, Standard Reductions
| | Jan 21 | FF II | ISWIM: lambda calculus, consistency, standard reductions
simplistic types and subject reduction
| | Jan 28 | Pierce 8, 9 | Simply Typed ISWIM: the nature of types
safety, type soundness, vectors and division
| | Feb 04 | Pierce 12 | Termination and Proof Theory
| | Feb 11 | Pierce 11, 13 | Simply typed functional extensions
Simply typed destructive updates
| | Feb 18 | Pierce 14, 15 | Simply typed exceptions
Subtyping
|
|