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: Linear types can change the world (1990)

A paper oft cited as the source of the practical use of linear types in programming languages. It builds up a basic linear type system and shows how you can unify this into a nonlinear world and build some non-trivial programs out of it. It also deals with how to allow having many read references alive to something, while still keeping write references linear.

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.5439&rep=rep1&type=pdf

Sub-structural types systems

Linear types can change the world! (1990)

A paper oft cited as the source of the practical use of linear types in programming languages. It builds up a basic linear type system and shows how you can unify this into a nonlinear world and build some non-trivial programs out of it. It also deals with how to allow having many read references alive to something, while still keeping write references linear.

Paper Link