COMP_SCI 396, 496: Type Systems

Quarter Offered

None ;


COMP_SCI 321 (mandatory)


The course assumes the background of 321 and will cover various type system material, including the polymorphic lambda calculus, Hindley-Milner type inference, dependent types, subtyping, and substructural types, which form the theoretical basis for the type systems of Java, Scala, Swift, OCaml, Coq, Agda, and Rust.

The course will draw on material from the research literature as well as textbooks. Expect to have to read original research papers on some of the topics. Homework will be those readings and two significant projects involving the implementation and use of two of the type systems that we cover.

  • This course fulfills the Technical Elective requirement.

COURSE INSTRUCTORS: Prof. Jesse Tov & Prof. Robby Findler