CS7480  Special Topics in PL: Type Systems

Spring 2012

Links

• Schedule
• Advanced Topics Presentations
• Research Themes

Course Information

Time & Place

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

Professor

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:

• Core topics: The first 7 weeks will consist of lectures by the instructor on core topics.
• Advanced topics: During the next 4 weeks, we will cover advanced topics chosen by the instructor by reading book chapters and/or research papers; these topics will be presented by students in the class.
• Research themes: During the final 4 weeks of the semester, students will give lectures on their chosen research theme.

Prerequisites

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

Textbooks

Readings will include chapters from the following books:

• Types and Programming Languages (TAPL), Benjamin C. Pierce, MIT Press, 2002.
• Advanced Topics in Types and Programming Languages (ATTAPL), edited by Benjamin C. Pierce, MIT Press, 2005.

Grading

Students will be evaluated on the basis of:

• homework assignments on core topics covered in the first part of the course (15%)
• an in-class lecture on one of the advanced topics and lecture notes to be distributed to the class (40%)
• investigation of a research theme, an annotated bibliography of the papers selected for presentation, and an in-class lecture on the chosen theme (45%)

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

Schedule

(Subject to change)

Date	Topic and Readings	Presenter	HW/Notes
W 1/11	Simply-typed lambda calculus; Type safety TAPL 8, 9	Amal
F 1/13	Products, sums, recursion, etc.; References TAPL 11, 13	Amal
W 1/18	Subtyping TAPL 15, 16	Amal
F 1/20	Recursive types TAPL 20	Amal
W 1/25	No class (POPL)
F 1/27	No class (POPL)
W 2/1	Strong normalization for STLC TAPL 12	Amal
F 2/3	Type safety via logical predicates; Step-indexed models	Amal	hw1 (latex)
W 2/8	Parametric polymorphism TAPL 23	Amal
F 2/10	Parametricity and free theorems	Amal
W 2/15	Curry-Howard isomorphism; Existential types Wadler; TAPL 9.4; TAPL 24	Amal
F 2/17	More Curry-Howard (continuations and negation); More existential types	Amal
W 2/22	Representation Independence; Contextual Equivalence	Amal
F 2/24	Step-indexed logical relations	Amal
W 2/29	ML Type Inference PLAI Ch 30-31, TAPL Ch 22	Tony Garnock-Jones	notes
F 3/2	Substructural Type Systems ATTAPL Ch 1 (required) Optional: L^3: A Linear Language with Locations, Morrisett et al., TLCA 2005, Sections 1-2 Optional: Substructural State, Ahmed et al., ICFP 2005, Sections 1-3	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	Type-Preserving Compilation, Types for Low-Level Languages From System F to Typed Assembly Language, Morrisett et al., TOPLAS 1999	Jamie Perconti	notes
F 3/16	Type-and-Effect Systems ATTAPL Ch 3 Optional: Marriage of Effects and Monads, Wadler and Theimann, ACM ToCL 2003	Asumu Takikawa	notes
W 3/21	Object Encodings Comparing Object Encodings, Bruce et al., Info. and Comp. 155(1/2):108-133, 1999 Type-Preserving Compilation of Featherweight Java, League et al., ACM TOPLAS 2002	Fabian Muehlboeck	notes
F 3/23	No class (PhD Open House)
W 3/28	Module Systems Dreyer's dissertion, Ch 1 F-ing Modules, Rossberg et al., TLDI 2010	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