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
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.
The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Software Verification — Andrew Appel
Category Theory — Lars Birkedal
Parametricity and Relational Reasoning — Derek Dreyer
Type Theory Foundations — Robert Harper
Programming in Agda — Ulf Norell
Certified Programming and State — Greg Morrisett
Proof Theory Foundations — Brigitte Pientka
Designing Dependently-Typed Programming Languages — Stephanie Weirich
Software Foundations in Coq — Steve Zdancewic