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.
Thorsten Altenkirch
— University of Nottingham Introduction to Type Theory Type Theory is at the same time an alternative to set theory as a mathematical foundation and a programming language originally conceived by the Swedish philosopher and mathematician Per Martin-Löf. The course is an introduction to Type Theory which covers the following topics:
I have a webpage for this series of lectures. Please see the instructions for installing Agda prior to OPLSS. |
Stephanie Balzer
— Carnegie Mellon University Session-Typed Concurrent Programming Message-passing is a successful concurrency paradigm that has been adopted by various practical languages such as Erlang, Go, and Rust. The Servo a browser engine developed in Rust, for example, exploits message-passing to heavily parallelize tasks that are executed sequentially in existing web browsers. Messages are exchanged along channels, which are typed with enumeration types. Whereas typing ensures that only messages of the appropriate type are communicated along channels, it fails to guarantee protocol adherence. Session types can be used to type communication channels to statically verify protocol adherence. Session types were introduced in the context of process calculi, but made their way into practical languages as libraries or embedded DSLs. In these lectures, we focus on a particular family of session types that stand in close correspondence with intuitionistic linear logic. We first focus on linear session types, which describe the communication protocols between a providing process and its client. We discover together their grounding in linear logic and the strong properties of protocol adherence and deadlock-freedom they entail. Then we extend the calculus to support shared session types, allowing a process to have multiple clients and accommodating a wider range of programming examples. Lastly, time permitting, we explore the application of session types to information flow control. Session types naturally constrain the flow of information. We develop a possible-world type system to ensure information flow control by type-checking, and, time permitting, work out the schema of a logical relation for proving noninterference. Participants interested in hands-on experience may want to check out Soares (Ruofei) Chen's OPLSS 2021 tutorial [1] on Ferrite [2, 3], a session type library in Rust.
[1]
https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php#chen
|
Adam Chlipala
— Massachusetts Institute of Technology From Type Theory to End-to-End Proof of Realistic Systems The foundations covered in this summer school feel like they should, in principle, be sufficient to justify the correctness of significant computer systems, but the devil is in the details. I will present some of those details, referencing implementation projects using the Coq proof assistant while focusing on the big ideas behind them. The goal of these projects is to produce unified correctness and security proofs of everything digital in nontrivial applications. The theorems stop at the point where we are about to think about geometry of hardware designs, instead covering gate-level processor descriptions and machine code, tracing back through to high-level relational specifications. Lectures will be divided across three main abstraction levels: high-level software, low-level software, and hardware. These levels are associated with interestingly different proof methods: equational reasoning, Hoare (separation) logic, and refinement of message-passing concurrent modules. One cross-cutting theme is cryptography, which will give me a chance to discuss our results that have been transitioned into broad use in open-source projects like Chrome and Firefox. |
Pierre-Louis Curien
— Institut de Recherche en Informatique Fondamentale Game Semantics The goal of the course is to illustrate the application of game semantics to the study of programming languages; in particular, how it naturally captures important aspects of program execution such as the interaction of a program with its environment. Lecture 1 | Lecture 1 handout | Lecture 1 notes Lecture 2 | Lecture 2 handout | Lecture 2 notes Lecture 3 | Lecture 3 handout | Lecture 3 notes |
Paul Downen
— University of Massachusetts, Lowell Abstract Machines and Classical Realizability Abstract machines give us a way to mathematically model the way computers think about our programs in terms of lower-level concepts, and help to specify how to correctly implement programming languages. These serve as the more implementation-oriented counterpart to tools like lambda calculus and type theory, that give us a mathematical model closer to the way that humans think about programs written in functional languages. You may think that going down to the low-level details of a machine would force us to lose all the nice reasoning tools that we can employ in thehigher level theories. But it does not! The goal of this lecture series is to introduce abstract machines as not just a tool for specifying language implementations, but also as a rich theory for reasoning about programs. This can be achieved through an application of *realizability* which extracts useful information out of mathematical theorems: reasoning principles can be implemented by real computer instructions and proofs can be justified by programs that construct evidence. We will be looking at the branch of realizability for constructive classical logic where classical axioms, such as double negation elimination or law of the excluded middle, can be implemented by specific computational effects that are easy to express in an abstract machine. Serendipitously, this same model of classical realizability also lets us reason about features of practical programming languages, including dynamic features (like computational effects and evaluation strategies) that help us run programs and static features (like (co)induction and subtyping) that help us to predict what programs would do ahead of time. Specific topics covered are:
Main lecture notes | Supplemental examples and background Lecture 1 | Lecture 1 (alternate angle) part 1 | Lecture 1 (alternate angle) part 2 | Notes | Lecture 2 | Lecture 2 (alternate angle) part 1 | Lecture 2 (alternate angle) part 2 Lecture 3 | Lecture 3 (alternate angle) part 1 | Lecture 3 (alternate angle) part 2 |
Silvia Ghilezan
— University of Novi Sad Rewriting and Termination in Lambda Calculus Rewriting comprises a wide range of methods of replacing subterms of a formula with other terms. Rewrite systems are present in logic, algebra, linguistics. Fundamental question of computation are addressed in rewriting, such as, confluence, termination, critical pairs, strategies. Consequently there is a huge variety of different rewrite systems.
Lambda calculus is a higher-order rewrite system
due to bound variables and higher-order functions.
|
Jeremy Gibbons
— University of Oxford Algebra of Programming Tony Hoare observed that program structure follows data structure. One manifestation of this phenomenon is the rich structure of patterns of computation that can be represented as datatype-generic programs, parametrized by the structure of the data they process. This course provides an introduction: folds and unfolds; hylomorphisms, histomorphisms, futumorphisms, etc; streaming and metamorphisms; traversals and effects. Lecture 1 | Lecture 1 notebook | Lecture 1 notes Lecture 2 | Lecture 2 notebook | Lecture 2 notes Lecture 3 | Lecture 3 (alt angle) part 1 | Lecture 3 (alt angle) part 2 | Lecture 3 notebook | Lecture 3 notes Lecture 4 | Lecture 4 (alt angle) part 1 | Lecture 4 (alt angle) part 2 | Lecture 4 notebook | Lecture 4 notes |
Robert Harper
— Carnegie Mellon University Introduction to the Theory of Logical Relations Logical relations, the main method for giving semantics to type theories, originated with Tait's "computability method", and has been greatly developed over many years in a variety of directions. The goal of these lectures is to give students an introduction to the main tools of the theory of logical relations, including Tait's original formulation, Girard's and Martin-Löf's extensions, Reynolds's theory of parametricity, and, time permitting, more recent extensions to proof-relevance and higher dimensions. |
Sam Lindley
— The University of Edinburgh Effect Handler Oriented Programming In software systems effects are pervasive, e.g.: concurrency, distribution, exceptions, I/O, and nondeterminism. Effect handlers are a general programming feature that can be used for modularly implementing all of these effects and more. They were introduced by theoretical computer scientists studying the theory of algebraic effects, but now show promise as a practical programming tool. Facebook's React.JS UI library relies on implementation strategies and abstractions directly inspired by effect handlers. Uber's Pyro tool depends on effect handlers for abstracting over probabilistic programming features. Github's Semantic library, which is used for code navigation on github.com, makes essential use of effect handlers. OCaml 5.0 includes a high-performance implementation of effect handlers, whose design has also inspired a proposal for extending WebAssembly with effect handlers as a uniform target for asynchronous and concurrent programming features. This course will cover the theory of algebraic effects and effect handlers, effect handler oriented programming by example, expressiveness of effect handlers, and effect encapsulation.
|
Frank Pfenning
— Carnegie Mellon University Introduction to Proof Theory
Lecture 3 | Lecture 3 (alt angle) part 1 | Lecture 3 (alt angle) part 2 | Lecture 3 notes |
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 |
Steve Zdancewic
— University of Pennsylvania Formal Verification of Monadic Computations This series of lectures will look at one appealing approach to specifying, implementing, and testing the behaviors of interactive systems. The idea is to build compositional, modular, and executable semantics by layering monadic interpreters and reasoning about them equationally. We will see how to work with and reason about effects like nontermination, state, and I/O, all within a pure, total dependent type theory such as Coq. This approach is embodied by the interaction trees library, which has been used for various verification efforts, including for web servers and compilers, as part of the DeepSpec project. The lectures will be accompanied by a Coq tutorial with exercises inspired by those applications. |