Class 3: Dependent Type Theory

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!

You can find a reading guide and some discussion questions below. Slides for the class are available here.

The non-optional lecture notes about Curry-Howard might seem a bit dense at times. I think the ideal is to get the basics out of it---like how implication in logic corresponds to the types of functions, and how modus ponens (if A implies B, and A, then B) corresponds to function application.

The section on reduction is important to grasp at a very high level, but not important to grasp the details of just yet. It will matter when we talk about equality, as one notion of equality in proof assistants like Coq amounts to "both terms reduce to the same thing," basically. But the details will not be quite the same; we'll cover that in class.

The other two readings are there for your enjoyment, if they help you, so make of them what you will.

Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):

1. What do you think are some of the tradeoffs of building proof assistant foundations based on a logic like in Isabelle/HOL, versus directly based on a type system like in Coq?
2. By Curry-Howard, proofs are programs. This opens up a whole world of tools that we build for programs that we might also be able to build for proofs. Can you think of any development tools or automation that we build for programs that might also be useful for proofs? What might it look like? This can be speculative---get creative about this.
3. From what you've learned so far about foundations, what would you consider in designing a modern proof assistant from scratch? Has this changed since reading about Curry-Howard and type-theory-based foundations?
4. Write a paragraph responding to someone else's comment in the discussion forum.
5. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.