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