CMSC 32001-1: Preliminary Outline
Spring, 2007

Algorithms and algorithmic analysis
Implementation techniques

Paradigmatic examples of functional type systems

* Example 1: simple typed lambda calculus

* Example 2: Hindley Milner let polymorphism

* Example 3:
  (a) System F, SOL type checker
  (b) Challenge: type inference for System F
      local type inference

SML/NJ -- a realistic example

* SML/NJ type checker
  type inference, unification, generalization, instantiation
  value restriction
  overloading (variables, literals)
  partial record patterns ({...})
  datatypes

* SML/NJ modules
  signatures and realizations
  higher-order functors

* FLINT type system
  translation to F-omega
  hash consing
  normalization and equivalence

* Extensions of SML type system
  first-class polymorphism (Laufer-Odersky, ...)
  fancy records, row-polymorphism
  (limited) subtyping
  type dynamic
  extensible datatypes

* Extensions of SML module system
  parametric signatures
  recursive modules


Conceptual topics

* type equivalence: structural, generative, nominal
* F^omega_sub (Cardelli implementation paper)
* Elaboration into typed intermediate languages (TILT)
* Types and effects
* Types and exception analysis
* Local type inference
* Type dynamic


Advanced or Optional topics (student presentations, projects)

* Haskell type system
  Type classes

* Moby type system and type checking
  impredicative, first-class polymorphism,
  subtyping,
  objects/modules

* TILT

* OCaml features:
  row polymorphism
  equirecursive types
  OCaml object system (classes, object types, subtyping)

* Object oriented languages
  subtyping, recursions, higher-order operators
    (bounded polymorphism, F-bounded polymorphism)
  Cook
  Cardelli, Bruce, Mitchell, Pierce
  Bruce languages
  Java, C# (generics)

* Exception analysis through typing (Leroy, Blume, ...)

* Type safe systems programming
  Modula 3
  Cyclone
  Safe C
  TAL
  PCC

* Mobile types
  Peter Sewell, Jamie Leifer, Gilles ?

* Static typing vs macros