University of Oregon University of Oregon

Oregon Programming Languages Summer School

Types, Semantics, and Logic

June 26-July 8, 2023

Types, Semantics, and Logic

June 26-July 8, 2023

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

Amal Ahmed — Northeastern University

Logical Relations

Lecture Notes

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

Lecture 4 video part 1 | part 2 | part 3

Sandrine Blazy

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.

Course Materials

Slides

Lecture 1 video part 1 | part 2 | part 3

Lecture 2 video part 1 | part 2 | part 3 | part 4 | blackboard | blackboard

Silvia Ghilezan

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:

Handouts (1) |

Lecture Notes (1) |

Handouts (2) |

Lecture 2 video part 1 | part 2 | part 3

Lecture Notes (2) |

Handouts (3)

Lecture 3 video part 1 | part 2 | part 3

Lecture Notes (3)

Marianna Girlando

Marianna Girlando — University of Amsterdam

Introduction to Proof Theory

Lecture Slides 1

Lecture 1 video part 1 | part 2 | part 3

Lecture Slides 2

Lecture 2 video part 1 | part 2 | part 3

Sonia Marin

Sonia Marin — University of Birmingham

Introduction to Proof Theory

Lecture Slides 3

Lecture 3 video part 1 | part 2 | part 3

Lecture Slides 4

Lecture 4 video part 1 | part 2 | part 3

Lecture Slides 5

Lecture 5 video part 1 | part 2 | part 3

Lecture Notes

Paige Randall North

Paige Randall North — Utrecht University

Introduction to HoTT

Github

Lecture 1 video part 1 | part 2 | part 3

Lecture Notes

Lecture 2 video part 1 | part 2 | part 3

Lecture 3 video part 1 | part 2 | part 3

Lecture 4 video part 1 | part 2 | part 3

Jennifer Paykin

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).

Github

Lecture 2 video part 1 | part 2 | part 3

Lecture 3 video part 1 | part 2

Lecture 4 video part 1 | part 2 | part 3

Lecture Notes

Daniela Petrisan

Daniela Petrisan — Institut de Recherche en Informatique Fondamentale

Introduction to Category Theory

Lecture Notes

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

Lecture 4 video part 1 | part 2 | part 3

Lecture 5 video part 1 | part 2 | part 3

Ruzica Piskac

Ruzica Piskac — Yale University

Program Synthesis

Lecture 1 Slides

Lecture 1 video part 1 | part 2 | part 3

Lecture 2 Slides

Lecture 2 video part 1 | part 2 | part 3

Lecture 3 Slides

Lecture 3 video part 1 | part 2 | part 3

Lecture 4 Slides

Lecture 4 video part 1 | part 2 | part 3

Lecture Notes

Sukyoung Ryu

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 Slides

Lecture 1 Notes

Lecture 1 video part 1 | part 2 | part 3

Lecture 2 Slides

Lecture 2 video part 1 | part 2 | part 3

Lecture 3 Slides

Lecture 3 video part 1 | part 2 |

Lecture 4 Slides

Lecture 4 video part 1 | part 2 | part 3

Stephanie Weirich

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

Lecture 1 video part 1 | part 2 | part 3

Lecture 1 questions