Preparation
Prior to OPLSS, students should have the following software ready on their laptops
Technical Lectures
The program consists of thirty-six 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Programming Languages Background — Robert Harper and Dan Licata
These two lecture series will cover foundational programming languages background that will prepare students for the later lectures. The topics that will be covered include operational semantics and type systems; function, product, sum and recursive types; polymorphism; concurrency; cost semantics; the logical relations proof method; parametricity. Practical Foundations for Programming Languages chapters 1-10, 14-20, 37-38, 46-48.
Category Theory Background — Ed Morehouse
These lectures will serve as an introduction to category theory and help prepare students for the subsequent lectures on categorical semantics. We will begin from the basic definitions and discuss duality, functors, universal constructions, natural transformations and adjunctions. We will use these concepts to construct a categorical semantics for the simply-typed lambda calculus. Throughout, we will emphasize the benefits of behavioral (versus structural) characterizations, and of diagrammatic reasoning.
Logical Relations — Patricia Johann
Reynolds' theory of parametricity for System F captures
the invariance of polymorphically typed programs under change of data representation.
Reflexive graph categories and fibrations are both known to give
a categorical understanding of parametricity.
In these lectures we will learn how bifibrations further contribute to this understanding.
Specifically, we will develop a bifibrational framework
for constructing models of System F that are parametric,
in the sense that
1) they generalize Reynolds' original parametric model for System F, and
2) they verify natural generalization of Reynolds' Identity Extension Lemma
and Abstraction Theorem, both of which are verified by his original model.
The models our framework constructs can also be shown to verify
other "litmus test" properties of parametric models —
such as the Graph Lemma, the existence of initial algebras and final coalgebras —
that are commonly used in applications.
Lecture 1 - Reynolds' Theory of Parametricity for System F
Lecture 2 - Introduction to (Bi)Fibrations
Lecture 3 - A Bifibrational View of Parametricity
Lecture 4 - Bifibrational Parametric Models for System F
Network Programming — Nate Foster
A lot of recent work has explored how ideas from programming languages and formal methods can be used to solve practical problems in networking. Languages such as FlowLog, Frenetic, Pyretic, Maple, Nettle, NetCore, etc. offer high-level abstractions for specifying network functionality, while verification frameworks such as Anteater, Batfish, Header Space Analysis, NetKAT, and Veriflow provide tools for checking invariants automatically. These lectures will provide a comprehensive introduction to the theory and practice of network programming. We will introduce mathematical models for network programming based on operational, denotational, and axiomatic techniques, and we will show how they can be used to specify and verify a variety of real-world applications. Other topics covered will include concurrency, consistency models, equational reasoning, coalgebraic techniques, and probabilistic semantics.
Automated Complexity Analysis — Jan Hoffmann
Resource usage— the amount of time, memory, and energy a program requires for its execution— is one of the central subjects of computer science. Nevertheless, resource usage often does not play a central role in classical programming-language concepts such as operational semantics, type systems, and program logics. I will revisit some of these concepts to model and analyze resource usage of programs in a formal and compositional way. An emphasis will be on practical, type-based techniques that automatically inform programmers about the resource usage of their code. Specifically, I will explain how the potential method of amortized analysis can be integrated into a type system of a simple functional language to automatically derive bounds that are polynomials in the sizes of the arguments.
Separation Logic and Concurrency — Aleks Nanevski
Separation logic has emerged as an effective logical framework for specifying and verifying pointer-manipulating programs. These lectures will start from the basic sequential separation logic as proposed by O'Hearn, Reynolds, and collaborators, and build on it to explain some of the main ideas behind the recently developed state of the art in the verification of shared-memory concurrency. Through many concrete examples, we will illustrate the specification and verification patterns that provide effective reasoning about lock-based and lock-free concurrent programs over pointer-based data structures, including linearizable and non-linearizable programs, and pointer structures with so-called "deep sharing" such as graphs. Along the way, we will point out the many high-level connections between separation logic and type theory.
Principles of Type Refinement — Noam Zeilberger
These lectures will introduce students to fundamental principles of type refinement systems, which are type systems designed from the idea of layering one type system on top of another. The first part will go over basic but important concepts such as the distinction between refinement and subtyping, while using datasort refinements and intersection and union types as illustrative examples. From there, we will turn to more advanced topics such as the role of refinement typing in characterizing dynamic behavior, the design of type refinement systems in the presence of computational effects, and bidirectional typechecking. The last part will revisit the foundations of type refinement from a categorical viewpoint. Here we will take a deliberately broad view of what constitutes a "type refinement system", as simply being a functor from one category to another. Through various motivating examples, we will work our way up to the definition of a monoidal closed bifibration, and illustrate its use as a powerful tool for analyzing a wide range of type refinement systems.
Logical relations/Compiler verification — Amal Ahmed
The logical relations proof method has been used to prove a wide range of properties, including type safety, equivalence of programs, noninterference (in security typed languages), and compiler correctness. Building on Dan Licata’s introduction to logical relations for the simply typed lambda calculus and System F, these lectures will discuss how to scale logical relations to Turing-complete languages with features such as recursive types and mutable state. We will develop a step-indexed logical relation for a language with recursive types, using step-indexing to ensure that the logical relation remains well-founded. We will then show how the idea of step-indexing can be used to avoid semantic circularities that arise when defining logical relations for languages with dynamically allocated mutable references. The lectures will also discuss how to establish that a logical relation corresponds to contextual equivalence. The lecture series will conclude with a look at how logical relations may be used in the realm of compositional compiler correctness using closure conversion as a case study.