CS7480  Special Topics in PL:
Gradual Typing and Principled Language Interoperability

Spring 2019

Course Information

Time & Place

Mondays and Wednesdays, 2:50pm - 4:30pm in Ryder Hall, Room 157


Amal Ahmed
Office: WVH 328
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 typing which allows statically typed and dynamically typed 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 --- more precisely and less precisely typed, high-level and low-level, and ones that support disparate type features. When developers mix components written in different programming languages, there is a question of how they ought to reason about the behavior of single-language components that will linked with code from other languages with different expressive power, and a question of how compiler and language design should evolve to make such reasoning easier for developers. 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 undergraduates are 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), or permission from instructor.


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, and participate in class discussion. They are also welcome to present a research paper. Talk to the instructor if you want to audit the course.


(Subject to change)

Date Topic and Readings Presenter HW/Notes
M 1/7
  • Simply-typed lambda calculus; Type safety
    TAPL 8, 9, 11
W 1/9
  • Strong normalization for STLC
    TAPL 12
M 1/14
  • Subtyping; References
    TAPL 15, 16, 13
Amal hw1 (latex)
W 1/16
  • No class (POPL'19)
M 1/21
  • No class (MLK day)
W 1/23
  • Recursive types; Step-indexed logical relations
    TAPL 20
F 1/25,   Ryder 433
(make-up day)
  • Polymorphism and existential types
    TAPL 23, 24
Amal hw1 due
M 1/28
  • Parametricity, free theorems, and representation independence
    Theorems for Free, Philip Wadler, FPCA 1989 (skip Section 7)
Amal hw2 (latex)
W 1/30
M 2/4 Julia Belyakova
W 2/6 Jay Kruer
M 2/11
  • No class (Amal at PLDI PC meeting)
hw2 due
W 2/13
  • Background reading: Dependent Types, ATTAPL Ch 2

  • Hybrid Type Checking
    Kenneth Knowles and Cormac Flanagan.
    TOPLAS 2010
Ankit Kumar
F 2/15,   Ryder 433
(make-up day)
Dustin Jamner
M 2/18
  • No class (President's day)
W 2/20 Ellen Arteca
F 2/22,   Ryder 433
(make-up day)
Alexi Turcotte
M 2/25 Artem Pelenitsyn
W 2/27 Ellen Arteca
M 3/4
  • No class (Spring break)
M 3/6
  • No class (Spring break)
M 3/11 Sam Caldwell
W 3/13 Julia Belyakova
M 3/18 Max New
W 3/20 Artem Pelenitsyn
M 3/25 Aaron Weiss
W 3/27 Hyeyoung Shin
M 4/1
  • No class
W 4/3 Michael Ballantyne
M 4/8 Hyeyoung Shin
W 4/10 Alexi Turcotte
Th 4/11,   Ryder 243
(make-up day)
Michael Ballantyne
M 4/15
  • No class (Patriot's day)
W 4/17 Amal
F 4/19,   Ryder 245
(make-up day)
Aaron Weiss

Additional Reading

Amal Ahmed
Last modified: Wed Apr 10 22:15:43 EDT 2019

Valid XHTML 1.0!