Description: Lecture, four hours; outside study, eight hours. Requisite: course 131. Introduction to static type systems and their usage in programming language design and software reliability. Operational semantics, simply-typed lambda calculus, type soundness proofs, types for mutable references, types for exceptions. Parametric polymorphism, let-bound polymorphism, polymorphic type inference. Types for objects, subtyping, combining parametric polymorphism and subtyping. Types for modules, parameterized modules. Formal specification and implementation of variety of type systems, as well as readings from recent research literature on modern applications of type systems. Letter grading.

Units: 4.0