Coq Preparation and Boot Camp
Several of the course lecture sequences will assume basic familiarity with the use of the Coq proof assistant. In particular, the lecture sequence Software Foundations in Coq, based on the book of the same name [available online], will begin at the chapter titled "Prop: Propositions and Evidence." Students without prior experience using Coq are strongly encouraged to install the software and study the earlier chapters of Software Foundations on their own before the school begins.
To help further prepare Coq beginners, the program will be preceded by Coq boot camp: a one-day, intensive, hands-on introduction to the practical mechanics of the proof assistant and its user interface. This session will be held on July 21. It will be led by Andrew Tolmach, and staffed by a team of experienced users. This boot camp will not be a substitute for prior self-study, but it should help solidify understanding of basic concepts and techniques, clear up practical questions, and give an opportunity to practice using the prover with expert help available.
Technical Lectures
The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Logical Relations — Amal Ahmed
Students should be familiar with the basics of simply-typed lambda calculus, recursive types, mutable references, and polymorphism at the level covered in Benjamin Pierce's Types and Programming Languages textbook (TAPL), chapters 9, 20, 13, and 23.
Additional recommended reading: TAPL chapter 12 on "Normalization" which shows how logical relations may be used to prove strong normalization for the simply-typed lambda calculus.
- Slides from lecture 6
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2] [part 3]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3]
- Lecture 5 [part 1] [part 2] [part 3] [part 4]
- Lecture 6 [part 1] [part 2] [part 3]
Type Theory Foundations — Robert Harper
These lectures will introduce intuitionistic dependent type theory. It would be helpful to have read Bengt Nordstroem's "Programming in Martin-Löf's Type Theory", which is available on the web at ITT, and the first two chapters of "Homotopy Type Theory", also available on the web at HoTT.
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2] [part 3]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3] [part 4]
- Lecture 5 [part 1] [part 2] [part 3]
Dependently-typed Programming in Agda — Dan Licata
Students should install Agda, following the direction at my OPLSS page Students might find it helfpul to peruse some of the tutorials listed there, but no prior knowledge of Agda will be assumed.
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2] [part 3] [part 4]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3] [part 4]
- Lecture 5 [part 1] [part 2] [part 3]
Adventures with types in Haskell — Simon Peyton-Jones
It will be an advantage if you have at least a passing familiarity with Haskell. If not, run through a tutorial, trying to include something on type classes.
Lecture Slides
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3]
Linear Logic and Session-based Concurrency — Frank Pfenning
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2] [part 3]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3]
- Lecture 5 [part 1] [part 2] [part 3]
Software Foundations in Coq — Andrew Tolmach
Lectures will roughly follow the sequence in the textbook Software Foundations, starting at the chapter "Prop: Propositions and Evidence."
Students should have installed Coq8.4 (see these notes for help), and worked through the preceding chapters (the Boot Camp will cover these, rapidly).
video
- Lecture 1 [part 1] [part 2]
- Lecture 2 [part 1] [part 2] [part 3]
- Lecture 3 [part 1] [part 2] [part 3]
- Lecture 4 [part 1] [part 2] [part 3]
Designing Dependently-Typed Programming Languages — Stephanie Weirich
Lecture materials will be presented through Haskell implementations of reference type checkers and interpreters. Students should have a basic reading knowledge of Haskell, including datatypes, type classes, and monads. Introductory material is available online; students should have a working installation of GHC on their laptops for the homework assignments.
video
- Lecture 1 [part 1] [part 2] [part 3]
- Lecture 2 [part 1] [part 2] [part 3]
- Lecture 3 [part 1] [part 2] [part 3]
Verifying LLVM Optimizations in Coq — Steve Zdancewic