The program consists of 80-minute lectures. Most days, there is also a 80 minute hands-on session for participants to work through exercises given in lecture.
Amal Ahmed — Northeastern University
Logical Relations
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3
Sandrine Blazy — University of Rennes
Verified Compilation
Deductive verification provides very strong guarantees that software is bug-free. Since the verification is usually done at the source level, the compiler becomes a weak link in the production of software. Verifying the compiler itself provides guarantees that no errors are introduced during compilation.
This course will first introduce the basics of verified compilation, using the Coq theorem prover. Then, it will present CompCert, a fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3 | part 4 | blackboard | blackboard
Silvia Ghilezan — University of Novi Sad
Introduction to Barendregt's Lambda Cube
The Lambda Cube is a framework introduced by Henk Barendregt to systematically investigate eight different systems of lambda calculi with types. The basic system is the lambda calculus with simple types and all other systems are obtained as its three-dimensional extensions with: polymorphic types, type operators and dependent types.
The lectures cover the following topics of the systems of the Lambda Cube:
- Fundamental properties (confluence, subject reduction, uniqueness of types)
- Strong Normalisation
- Expressiveness
- Curry-Howard correspondence (formulae-as-types, proofs-as-terms)
Lecture 2 video part 1 | part 2 | part 3
Marianna Girlando — University of Amsterdam
Introduction to Proof Theory
Sonia Marin — University of Birmingham
Introduction to Proof Theory
Lecture 3 video part 1 | part 2 | part 3
Lecture 4 video part 1 | part 2 | part 3
Paige Randall North — Utrecht University
Introduction to HoTT
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3
Jennifer Paykin — Intel
Introduction to Coq
Coq is an interactive theorem prover that can be used to develop mechanized proofs of correctness for software systems. It uses dependent types and proof tactics to state and prove theorems about functional programs. This course will introduce Coq and the basics of interactive theorem provers through hands-on exercises and labs based on the Software Foundations curriculum.
Please install the Coq theorem prover (version 8.16 or later) on your system before OPLSS so that you are ready to engage in the course and the accompanying lab sessions. You can find instructions for installing Coq at https://coq.inria.fr/download. Please ensure you also have access to an IDE for working with Coq scripts e.g. CoqIDE (included in most Coq distributions), ProofGeneral (an emacs plugin), or VSCoq (a VSCode extension).
Lecture 2 video part 1 | part 2 | part 3
Lecture 3 video part 1 | part 2
Daniela Petrisan — Institut de Recherche en Informatique Fondamentale
Introduction to Category Theory
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3
Lecture 3 video part 1 | part 2 | part 3
Ruzica Piskac — Yale University
Program Synthesis
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3
Lecture 3 video part 1 | part 2 | part 3
Sukyoung Ryu — KAIST
Program Analysis
Program analysis estimates the behaviors of programs even without running them. This course will introduce fundamental theories, designs, and implementations of program analysis and share its real-world applications.
Lecture 1 video part 1 | part 2 | part 3
Lecture 2 video part 1 | part 2 | part 3
Stephanie Weirich — University of Pennsylvania
Implementing Dependent Types in pi-forall
Sometimes it takes a little coding to really understand what is going on. This course will help students approach type systems through a demo implementation of a simple dependently-typed programming language, called pi-forall, using Haskell. The focus of the lectures will be on the pi-forall type checker and how we can take mathematical descriptions of typing rules and turn them into programming systems.
Lectures and homework will be based on the tutorial implementation available at https://github.com/sweirich/pi-forall