3810 W '02
Send Mail
Read Mail


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.

Jan 02n/a
Jan 07FF I
Inductive Definitions, Inductive Proofs
Reductions, Calculi, Standard Reductions
Jan 21FF II
ISWIM: lambda calculus, consistency, standard reductions
simplistic types and subject reduction
Jan 28Pierce 8, 9
Simply Typed ISWIM: the nature of types
safety, type soundness, vectors and division
Feb 04Pierce 12
Termination and Proof Theory
Feb 11Pierce 11, 13
Simply typed functional extensions
Simply typed destructive updates
Feb 18Pierce 14, 15
Simply typed exceptions

last updated on Thu Feb 28 17:51:52 EST 2002generated with PLT Scheme