Preparation
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.
Prior to OPLSS, students should have the following software ready on their laptops The following software is recommended, although it is not required- Proof General
- Haskell Platorm (includes GHC and Cabal)
Coq Boot Camp
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 June 15 . It will be led by Michael Clarkson 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. Participation in the Coq Boot Camp is optional for OPLSS participants.
Lecture Schedule
Technical Lectures
The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Software Verification — Andrew Appel
Lecture 1
video1 |
video2 |
Lecture 2
video1 |
video2 |
Lecture 3
video1 |
video2 |
Lecture 4
video1 |
video2 |
Category Theory — Lars Birkedal
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
Lecture 4
video1 |
video2 |
video3
Lecture 5
video1 |
video2
Parametricity and Relational Reasoning — Derek Dreyer
Lecture 1
Left Board |
Right Board |
Slides |
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Type Theory Foundations — Robert Harper
Preparation Notes
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Programming in Agda — Ulf Norell
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Certified Programming and State — Greg Morrisett
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Proof Theory Foundations — Brigitte Pientka
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Designing Dependently-Typed Programming Languages — Stephanie Weirich
Pi-Forall on github
Lecture 1
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3
Software Foundations in Coq — Steve Zdancewic
Lecture 1
slides |
video1 |
video2 |
video3
Lecture 2
video1 |
video2 |
video3
Lecture 3
video1 |
video2 |
video3
Lecture 4
video1 |
video2 |
video3