CS7480  Special Topics in PL: Type Systems

Spring 2012

Course Information

Time & Place

Classes meet on Wednesday and Friday, 11:45am - 1:25pm in Richards 165.


Amal Ahmed
Office: WVH 328
Phone: 373-2076
Email: amal at ccs.neu.edu
Office hours: by appointment (email me)

Course Description and Requirements

A type system is a syntactic method for preventing some class of execution errors during the running of a program. Type systems in languages like Java and C# provide a lightweight tool for ruling out erroneous uses of data and illegal memory accesses. More sophisticated type systems can be used to guarantee a multitude of other properties, including confidentiality and integrity of data, atomicity in concurrent programs, safe execution of untrusted code, authenticity properties of cryptographic protocols, and differential privacy. Types have also been used for reasoning about memory management and resource usage, for verification of device drivers, for safe low-level systems programming, and much more.

This course will introduce students to the basic vocabulary and techniques associated with type systems and provide a taste of several advanced topics from the type systems literature. In addition, students will be expected to investigate a particular research theme by studying a series of research papers. They will be required to prepare an annotated bibliography and give a lecture presenting a summary and evaluation of 3 to 5 papers at the end of the semester.

The course consists of three parts:


CS 5400 (PPL) or CS 7400 (Intensive PPL)


Readings will include chapters from the following books:


Students will be evaluated on the basis of:

Auditors are welcome. Talk to the instructor if you want to audit the course or to just sit in on a few classes.


(Subject to change)

Date Topic and Readings Presenter HW/Notes
W 1/11
  • Simply-typed lambda calculus; Type safety
    TAPL 8, 9
F 1/13
  • Products, sums, recursion, etc.; References
    TAPL 11, 13
W 1/18
  • Subtyping
    TAPL 15, 16
F 1/20
  • Recursive types
    TAPL 20
W 1/25
  • No class (POPL)
F 1/27
  • No class (POPL)
W 2/1
  • Strong normalization for STLC
    TAPL 12
F 2/3
  • Type safety via logical predicates; Step-indexed models
Amal hw1 (latex)
W 2/8
  • Parametric polymorphism
    TAPL 23
F 2/10
  • Parametricity and free theorems
W 2/15
  • Curry-Howard isomorphism; Existential types
    Wadler; TAPL 9.4; TAPL 24
F 2/17
  • More Curry-Howard (continuations and negation); More existential types
W 2/22
  • Representation Independence; Contextual Equivalence
F 2/24
  • Step-indexed logical relations
W 2/29
  • ML Type Inference
    PLAI Ch 30-31, TAPL Ch 22
Tony Garnock-Jones notes
F 3/2 Justin Slepak notes
W 3/7
  • No class
Th 3/8
  • F-omega
    TAPL 29,30,31
Vincent St-Amour notes
F 3/9
  • Dependent Types
    ATTAPL Ch 2
Paul Stansifer notes
W 3/14 Jamie Perconti notes
F 3/16 Asumu Takikawa notes
W 3/21 Fabian Muehlboeck notes
F 3/23
  • No class (PhD Open House)
W 3/28 Jonathan Schuster notes
F 3/30
  • Session Types
Tony Garnock-Jones notes
W 4/4
  • Types for Binding and Open Terms
Paul Stansifer notes
F 4/6
  • Types for Low-Level Languages
Justin Slepak notes
W 4/11
  • Ownership Types
Fabian Muehlboeck notes
F 4/13
  • Types for Functional Reactive Programming (FRP)
Jonathan Schuster notes
W 4/18
  • Dependent Types for State (Hoare Type Theory)
Jamie Perconti notes
F 4/20
  • Types for Delimited Control Operators
Asumu Takikawa notes
W 4/25
  • Types for Optimization (Deforestation)
Vincent St-Amour notes

Amal Ahmed
Last modified: Mon Apr 16 14:44:08 EDT 2012

Valid XHTML 1.0!