For this class, we will read one not optional reading: these lecture notes about Curry-Howard by Frank Pfenning. We will complement this with two optional readings: Chapters 1 and 2 of The Calculus of Constructions by Thierry Coquand and Gérard Huet, and Chapter 2.1 of my PhD thesis.
This lecture will cover a lot of material pretty quickly: (1) the Curry-Howard Correspondence, (2) the dependent type theory that forms the basis of Coq, Agda, and Lean, and (3) different notions of equality and their implications. That's a lot, like an entire course worth of material in one lecture. It's OK not to understand all of it, I promise. I just want to get you started.
The not optional reading is all about Curry-Howard, which relates programs and type systems to proofs and logical systems. It's probably my favorite thing about all of programming languages, and what got me into this field to begin with. It also has really cool implications for how one can implement a programming language that is also a proof assistant. And we'll get a chance to play with a language like that on Thursday---a minimal language with relatively little automation built on top of it (Agda).
The two optional readings are there to give you a sense of the dependent type theory beneath Coq in particular (the Calculus of Inductive Constructions, or CIC), but we will for sure cover the basics in class.
The first artifact is Thursday. Don't forget to install it ahead of time!