Types, Semantics, and Program Reasoning

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:

• (Simply typed) λ-calculus and combinatory logic
• Propositions as types
• Classical vs intuitionistic reasoning
• Dependent types, Π- and Σ-types
• Reasoning in Type Theory, Equality
• Inductive and coinductive types
• Universes and paradoxes

I have a webpage for this series of lectures. Please see the instructions for installing Agda prior to OPLSS.

Lecture 1 | Lecture 1 notes

Lecture 2

Lecture 3 | Lecture 3 notes

Lecture 4 | Lecture 4 notes

Lecture 5 | Lecture 5 notes

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
[2] https://github.com/ferrite-rs/ferrite
[3] https://drops.dagstuhl.de/opus/volltexte/2022/16250/

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.

Lecture 1 | Lecture 1 (alternate angle) | Lecture 1 notes

Lecture 2

Lecture 3

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.

Course Notes

Lecture 1 | Lecture 1 handout | Lecture 1 notes

Lecture 2 | Lecture 2 handout | Lecture 2 notes

Lecture 3 | Lecture 3 handout | Lecture 3 notes

Lecture 4 | Lecture 4 handout | Lecture 4 notes

Lecture 5 | Lecture 5 handout | Lecture 5 notes

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:

• Simple abstract machines for modeling implementations of lambda calculus and functional languages
• Modeling computational effects and control flow in abstract machines
• Type theories and equational theories for abstract machine languages
• Orthogonality: commands that are safe to run, producers and consumers that can be safely connected
• Self-orthogonal candidates: models of types as sound and complete classifications of producers and consumers
• Orthogonality versus intuitionistic negation versus functional continuations
• Classical logic: realizing classical axioms as effectful instructions
• Refinement and subtyping: the two lattices of self-orthogonal candidates
• The impact of evaluation strategy and computational effects on self-orthogonal candidates
• Non-deterministic reduction of classical logic: fixed-point solutions to the safety
• Self-orthogonal models of inductive and coinductive types
• Self-orthogonal models of intersection and union types

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

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.
The addressed topics are:

• Confluence: Church-Rosser property, local confluence
• Normalisation: strong normalisation, head normalisation
• Strategies: leftmost-outermost strategy, perpetual strategies
• Simple types in lambda calculus: strong normalization
• Intersection types in lambda calculus: complete characterisations of normalisations

Lecture 1 | handout | notes

Lecture 2 | Lecture 2 (alternate angle) | handout | notes

Lecture3 | handout | notes

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

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.

Course Notes

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.

• Lecture 1: Introduction to algebraic effects and effect handlers

  I'll give an introduction to algebraic effects and effect handlers as a general approach to programming and reasoning about effectful computation. I'll present the notion of a computation over an algebraic effect as a command-response tree over an effect signature quotiented by some equational theory. I'll consider how to interpret command-response trees and motivate effect handlers as the reification of such interpretations as an object language feature that provides a generic implementation strategy for algebraic effects. I'll give examples to show that it can be useful to interpret the same command-response tree using different interpretations which may not respect the same equational theory. Thus effect handlers can provide an expressive programming feature independently of any non-trivial algebraic theory.

  Lecture 1 video | Lecture 1 notes

• Lecture 2: Effect handler oriented programming by example

  I'll give an overview of effect handler oriented programming by way of a collection of examples and a small-step operational semantics. I'll focus on concurrency examples, illustrating how effect handlers provide a flexible foundation for composing and customising a range of different concurrency abstractions.

  Lecture 2 video | Lecture 2 notes

• Lecture 3: Expressiveness of effect handlers

  I'll explore the expressiveness of effect handlers. I'll compare effect handlers with delimited control and monadic reflection. I'll compare different varieties of effect handlers including deep handlers, shallow handlers, and a hybrid form of handler, "sheep handlers", which form the basis of the WebAssembly proposal. If we have time I'll briefly outline a fundamental complexity result, showing that adding effect handlers to a pure functional programming language gives an asymptotic performance improvement for certain classes of algorithm.

  Lecture 3 notes

• Lecture 4: Effect encapsulation

  I'll describe some of the challenges of modular programming with effect handlers in practice. I'll discuss the design of effect type systems for effect handlers as a tool for taming the complexity of effect handlers when programming in the large. I'll illustrate the "effect pollution" problem that arises if one naively composes effect handlers, and explain how to alleviate it through various forms of effect encapsulation.

  Lecture 4 notes
  Links:cooperative concurrency
  Frank:cooperative concurrency
  Frank:pipes
  Frank:effect pollution

Introduction to Proof Theory

• Basics
  • natural deduction and sequent calculus
  • normalization and cut elimination
  • proofs as programs, proof reduction as computation
• Advanced (as time permits)
  • Polarization and focusing; call-by-push-value as a synthesis of call-by-name and call-by-value
  • Substructural and adjoint logics; message-passing concurrency
  • Axiomatic and semi-axiomatic sequent calculus; futures
  • Logic and memory layout
  • Circular proofs and recursion

Lecture 1 | Lecture 1 notes

Lecture 2

Lecture 3 | Lecture 3 (alt angle) part 1 | Lecture 3 (alt angle) part 2 | Lecture 3 notes

Lecture 4 | Lecture 4 notes

Lecture 5 | Lecture 5 notes

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

Lecture 2

Lecture 3

Lecture 4 part 1 | Lecture 4 part 2

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.

Lecture 1 | Lecture 1 (alternate angle) | Lecture 1 notes

Lecture 2