It is said that no two programming language experts can agree on the definition of the term “type system”. In short, type systems are simply a static categorization of values in a programming language, but in practice the details of a type system substantially influence how one writes software. In this course we will study the breadth of type system research, from classic erasable types and type inference to refinement types and gradual typing, looking at type systems not as mathematical entities but as tools. We will try to abstract the type systems from the languages and understand how and when types help programmers, implementers and language designers.

Course details

This course is being taught by Gregor Richards in Spring 2017. Office hours are by request; please email me at . Note that due to conference scheduling, this course will have a two week break, and to make up for that lost time, six weeks with slightly longer sessions (two hours instead of one and a half). The six extended weeks will start with the third week.

This is a reading course. Students are expected to read research papers in the domain of type systems. The first week or two will be a crash course on the underlying theory, simply to make the papers approachable, but this is not a theory course. Students will present one or two papers (depending on number of students) and are expected to read and participate in the discussion of all papers. As a final project, students will be expected to write either a short paper in the subject or a relevant piece of software. Students are expected to be familiar with the basics of compiler construction, formal language definition (i.e., context-free languages) and set theory.

This is the first time this course has been taught, so details are subject to change.

As an example of modestly-sophisticated language semantics, I've provided the Big Dumb Language. It has just enough features to show most of the interesting aspects of program semantics and typing, but no more.



This schedule remains up to date for those selections that have already been made.

05-16Abel Nieto RodriguezEstablishing object invariants with delayed types
Petri VarsaTypestate-oriented programming
05-18Ifaz KabirLinear Types Can Change the World!
Stephen LiBuilding and using pluggable type-checkers
05-25Rafi AlamPractical pluggable types for java
Yetian WangTowards Typed Prolog
05-30Sean HarrapReim & ReImInfer: checking and inference of reference immutability and method purity
Matt AmyA modal analysis of staged computation
06-01Zijin LiGeneralized typestate checking using set interfaces and pluggable analyses
Jose SernaThe chemical approach to typestate-oriented programming
06-06Zhichao YangThe design and implementation of typed scheme
Kaiyu WuDesign and evaluation of gradual typing for python
06-08Jichen ZhaoExternal Uniqueness Is Unique Enough
Jia Rong WuRegion-based memory management in cyclone
06-13Yuhao DongOwnership types for safe programming: preventing data races and deadlocks
06-27Petri VarsaStrongtalk: Typechecking Smalltalk in a Production Environment
-General discussion on implementation
06-29Stephen LiTrace Typing: An Approach for Evaluating Retrofitted Type Systems
Yuhao DongAccepting Blame for Safe Tunneled Exceptions
07-04Kaiyu WuJust-in-time static type checking for dynamic languages
Jichen ZhaoLJGS: Gradual Security Types for Object-Oriented Languages
07-06Sean HarrapPatina: A Formalization of the Rust Programming Language
-General discussion
07-11Zijin LiEliminating array bound checking through dependent types
Jose SernaCayenne—a language with dependent types
07-13Matt AmyDependent types for program termination verification
Rafi AlamFoundations of path-dependent types
07-18Jia Rong WuAlias Types
Yetian WangModelling the Semantic Web using a Type System
07-20Ifaz KabirProgramming with polymorphic variants
Abel RodriguezColored local type inference
07-25 -Closing and general discussion


Students may present any on-topic paper. Simply ask me if a paper is relevant. As a hint, if it has a type soundness proof, it is almost certainly relevant!

The following is a list of suggested papers. I've tried to keep it to fairly recent work, and not included seminal work in various subfields of types. Note that due to my own biases, there is a heavy slant towards gradual typing and dynamic languages, but there's no reason that the actual papers selected have to have any such slant. You do not need to select a paper from this list; they are merely food for thought.