CS7480  Special Topics in PL:
Types, Contracts, Gradual Typing, and Compiler Correctness

Fall 2015

Course Information

Time & Place

Tuesdays (11:45am - 1:25pm) and Thursdays (2:50pm - 4:30pm) in Richards 233.


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

Course Description and Requirements

Static and dynamic typing offer complementary advantages: static typing (as in Java, C#, or ML) provides early error detection, efficient execution, and better documentation of code, whereas dynamic typing (as in various scripting languages) encourages rapid development and makes it easier to adapt to changing requirements. Traditionally, programming languages have supported either static or dynamic typing, but not both. Over the last decade there has been a flurry of research on gradual type systems that allow statically checked and dynamically checked components to be freely mixed. Another kind of mixing happens in multi-language software systems which are assembled using components written in different programming languages --- statically typed and dynamically typed, high-level and low-level. Formally reasoning about how components from such different languages should interoperate becomes essential when verifying correct compilation of components that may be linked with code compiled from other languages. This course seeks to cover this spectrum of interconnected issues.

Topics include:
The course is a research seminar that primarily focuses on reading and discussing papers from the scientific literature. The instructor will cover the basic vocabulary and techniques associated with type systems during the first three weeks. After that, at each class meeting, a student will be responsible for presenting a research paper. All students will be required to read the paper, submit a short critique of the paper before class, and come to class prepared to discuss the reading in depth.

This course is intended primarily for PhD students; however, MS students and as well as advanced undergraduates as welcome. Familiarity with programming language semantics and type systems (as covered in cs5400 or cs7400), or a willingness to pick up the material --- see background reading notes below --- is required, since most of the readings assume basic familiarity with these. If you are a first or second year Ph.D student interested in taking this course, but you have not yet taken cs7400 (IPPL), I would nonetheless encourage you to take this class as it will only be offered this once.


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


Readings will include a few chapters from the following books:


Students will be evaluated on the basis of

Background Reading

To pick up the background material required for this course you should read one of the following:


Auditors are welcome. Auditors will be expected to do the readings, submit critiques, and participate in class discussion. Talk to the instructor if you want to audit the course.


(Subject to change)

Date Topic and Readings Presenter HW/Notes
Th 9/10
  • Simply-typed lambda calculus; Type safety
    TAPL 8, 9, 11
Tu 9/15
  • Strong normalization for STLC
    TAPL 12
Th 9/17
  • Subtyping; References
    TAPL 15, 16, 13
Amal hw1 (latex)
Tu 9/22
  • Recursive types; Step-indexed logical relations
    TAPL 20
Th 9/24
  • Polymorphism and existential types
    TAPL 23, 24
Tu 9/29
  • Parametricity, free theorems, and representation independence
    Theorems for Free, Philip Wadler, FPCA 1989 (skip Section 7)
Amal hw2 (latex)
Th 10/1 Max New
Tu 10/6 Ben Chung
Th 10/8 Leif Andersen
Tu 10/13 James McNamara
Th 10/15 Nate Lilienthal
Tu 10/20 Matt Kolosick
Th 10/22 Nick Rioux
Tu 10/27 Vishesh Yadav
Th 10/29 William Bowman
Tu 11/3 Dustin Jamner
Th 11/5 Matt Singer
Tu 11/10 Kevin Clancy
Th 11/12 Sam Caldwell
Tu 11/17 Andrew Cobb
Th 11/19 Ben Greenman
Tu 11/24 Amal
Th 11/26
  • No class (Thanksgiving)
Tu 12/1 Brian LaChance
Th 12/3 William Bowman
Tu 12/8 Konstantinos Athanasiou
Th 12/10 Max New

Additional Reading

Amal Ahmed
Last modified: Fri Sep 25 10:54:23 EDT 2015

Valid XHTML 1.0!