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.
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-16||Abel Nieto Rodriguez||Establishing object invariants with delayed types|
|Petri Varsa||Typestate-oriented programming|
|05-18||Ifaz Kabir||Linear Types Can Change the World!|
|Stephen Li||Building and using pluggable type-checkers|
|05-25||Rafi Alam||Practical pluggable types for java|
|Yetian Wang||Towards Typed Prolog|
|05-30||Sean Harrap||Reim & ReImInfer: checking and inference of reference immutability and method purity|
|Matt Amy||A modal analysis of staged computation|
|06-01||Zijin Li||Generalized typestate checking using set interfaces and pluggable analyses|
|Jose Serna||The chemical approach to typestate-oriented programming|
|06-06||Zhichao Yang||The design and implementation of typed scheme|
|Kaiyu Wu||Design and evaluation of gradual typing for python|
|06-08||Jichen Zhao||External Uniqueness Is Unique Enough|
|Jia Rong Wu||Region-based memory management in cyclone|
|06-13||Yuhao Dong||Ownership types for safe programming: preventing data races and deadlocks|
|06-27||Petri Varsa||Strongtalk: Typechecking Smalltalk in a Production Environment|
|-||General discussion on implementation|
|06-29||Stephen Li||Trace Typing: An Approach for Evaluating Retrofitted Type Systems|
|Yuhao Dong||Accepting Blame for Safe Tunneled Exceptions|
|07-04||Kaiyu Wu||Just-in-time static type checking for dynamic languages|
|Jichen Zhao||LJGS: Gradual Security Types for Object-Oriented Languages|
|07-06||Sean Harrap||Patina: A Formalization of the Rust Programming Language|
|07-11||Zijin Li||Eliminating array bound checking through dependent types|
|Jose Serna||Cayenne—a language with dependent types|
|07-13||Matt Amy||Dependent types for program termination verification|
|Rafi Alam||Foundations of path-dependent types|
|07-18||Jia Rong Wu||Alias Types|
|Yetian Wang||Modelling the Semantic Web using a Type System|
|07-20||Ifaz Kabir||Programming with polymorphic variants|
|Abel Rodriguez||Colored 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.