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)
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