PL DiRP Spring 2023 Reading List

Week 1: Types and Programming Languages

Skim Chapter 1

I think that this provides a good high-level overview for generally what type systems are in programming languages, why they are useful, and what their shortcomings can be.

I think skimming this gives some good context for a kind of tool that is available to the programming languages researcher.

Skim Chapter 8

Gives a super simple introduction to how to go about defining a type system. Understand the notion of a program being "stuck", and how proving progress and preservation, let's you prove "safety". Don't get to bogged down in understanding all the proofs. Learn how to read typing rules.

Read Chapter 9.1-9.3

If you are unfamiliar with lambda calculus, skim Chapter 5. Understand basically how the simply typed lambda calculus's type system works. Don't spend too much time on it though, we'll go over it together if it's confusing. Think about what safety means for simply typed lambda calculus. How does the type system let us prove properties about non-terminating programs? If we implemented a checker for this type system, why would it not run forever on non-terminating programs?

Week 2:

Sub-structural types systems

Linear types can change the world! (1990)

An early paper on linear types in functional languages. Often cited as the beginning of this line of work


Cyclone Paper

Linear Regions are all you need (2006)

Seems like an interesting re-framing of an early rust type system


Original Rust paper

Rustbelt (2018)

Dahlia Paper (time-sensitive affine types)

Space time paper (Aetherling)

Effect Systems

A good bibliography: link

As of yet uncategorized

Granule (Quantitative Program Reasoning with Graded Modal Types)