The program consists of 80-minute lectures. We will also have some evening lectures, on topics of broader interest. Some days, there is also a hands-on session for participants to work through exercises given in lecture.
All lectures will be held in Room B50 of the Stone Science Building.
Amal Ahmed — Northeastern University
Semantic Type Soundness and Language Interoperability
This series of lectures will cover the use of logical relations to prove semantic type soundness of programming languages with increasingly advanced features and then show how a twist on the same technique can be can be employed to verify the soundness of foreign-function interfaces and language interoperability. Specifically, we will start with type soundness of a simply typed language. Then, we will move on to type soundness of languages with recursive types and mutable references, two features that introduce circularities that require us to make use of step-indexed logical relations. The last two lectures will cover proving soundness of language interoperability by verifying soundness of the target-level glue code that actually implements an FFI between two languages. For this we will devise a logical relation indexed by source-language types and inhabited by target-language terms — so-called realizability relations. I'll conclude with a discussion of why I think these realizability relations will have the same kind of outsize impact that step-indexed logical relations have had over the last two decades.
Lecture 1 Video
Lecture 2 Video
Lecture 3 Video
Lecture 4 Video
Lecture 5 Video
Arvind — Massachusetts Institute of Technology
Thomas Bourgeat — École Polytechnique Fédérale de Lausanne
Rule-based languages: from modular design to modular verification
- Introduction to rule-based languages by example. Designing hardware is about careful composition of sequential machines. Rule-based hardware languages, like Bluespec, use atomic rules, a nonstructural method of composition which embodies communication protocols between modules. We will demonstrate the advantage that such a method of composition offers against standard structural circuit composition.
- Design: In-order processor in rule-based languages. In-order processors operate on multiple instructions at the same time: while a new instruction is being fetched from memory, an older instruction is being decoded, and a still older instruction is being executed. Even the simplest pipelined processor embodies speculation, which introduce interesting nondeterminism. We will see how to describe such machines in rule-based languages.
- Metatheory: the refinement theorem, cornerstone of hardware modular verification In this lecture we will show how rule-based languages can be equipped with a semantic that provides the same modularity as software languages: despite the intrinsic parallelism of the hardware language, each module can be given a specification one method at a time. This will give us a refinement principle allowing us to replace a submodule by its specification, when working on the correctness of a parent module.
- Verification: A first proof of refinement We will write refinement proofs between two simple systems. We will explore two proof techniques: from an explicit invariant proof to a more implicitly derivable invariant. We will then extend our simple systems to slightly more sophisticated designs, and show the emergence of the need of what we call generalized specifications.
Lecture 1 Video
Lecture 2 Video
Lecture 3 Video
Chris Casinghino — Jane Street
Making OCaml Safe for Performance Engineering
Over the last couple of years, Jane Street has greatly increased its investment in OCaml, and has started developing major extensions to the OCaml's type system, with the primary goal of making OCaml a better language for writing high-performance systems.
In this talk, I'll attempt to provide a developer's-eye view of these changes. We'll cover two major directions of innovation: first, the addition of modal types to OCaml, which opens up a variety of ambitious features, like memory-safe stack-allocation; type-level tracking of effects, and data-race freedom guarantees for multicore code. The second is the addition of a kind system to OCaml, which will provides more control over the representation of memory, in particular allowing for structured data to be represented in a cache-and-prefetch-friendly tabular form. Together, these features pull together some of the most important features for writing high performance code in Rust, while maintaining the relative simplicity of programming in OCaml.
Stephen Chong — Harvard University
Language-Based Security
Programming Language techniques are a great fit for specifying, modeling, reasoning about, and building secure computer systems. In this series of lectures we will survey topics in Language-Based Security, including information-flow control, reasoning about cryptographic protocols, enforcing language abstractions, and more.
Lecture 1 Video | Lecture Slides | Student Notes
Lecture 2 Video | Lecture Slides | Student Notes
Lecture 3 Video | Lecture Slides | Student Notes
Lecture 4 Video | Lecture Slides | Student Notes
Paul Downen — University of Massachusetts, Lowell
Foundations of Programming Languages
We use programming languages to precisely define our programs, what they should do, and how they should operate. But how do we define a programming language itself? This lecture series introduces the common tools and techniques that we use to understand and prove properties about programs, the languages we use to express them, and the implementations of those languages. The focus will be on syntactic methods that avoid the need for complex mathematical machinery and are commonly used among programming language researchers, including: structural induction, operational semantics, type systems, rewriting theories, and abstract machines. Despite their modest nature, these tools are applied to make precise mathematical statements about complex program behavior like type safety, polymorphism and modularity, program equality, and computational effects. In the end, we will get a view of the language we use to express languages.
Foundations of Programming Languages
Lecture 1 cancelled due to campus power failure
Lecture 2 Video | Student Notes
Lecture 3 Video | Student Notes
Lecture 4 Video | Student Notes
Lecture 5 Video | Student Notes
Steven Holtzen — Northeastern University
Probabilistic Programming from the Ground Up
Probabilistic systems are notoriously difficult to reason about, but this doesn't stop people from making them: machine learning practitioners and scientists make probabilistic models for reasoning about the world, and software developers use randomness in designing their algorithms. What are the principles for designing scalable systems and tools to aid in the development, verification, and application of probabilistic uncertainty across today's software stack? To tackle this challenge, in this lecture series we will see the essential foundations of probabilistic programming languages: languages that are imbued with a first-class notion of probabilistic uncertainty.
We will discuss
- The syntax, semantics, and applications of probabilistic programming languages;
- The design of exact and approximate inference algorithms for reasoning under uncertainty;
- Foundations of static analysis tools for reasoning about a probabilistic program's behavior
After the lectures, you will be able to implement your own probabilistic programming language from scratch and understand the design space of this new and exciting class of programming languages.
Lecture 1 Video | Lecture Slides | Student Notes
Lecture 2 Video | Lecture Slides | Student Notes
Lecture 3 Video | Student Notes
Lecture 4 Video | Student Notes
Ever wonder what it's like to build a language in the wild? This talk will cover lessons learned from over 13 years working on the Rust Programming Language.
Frank Pfenning — Carnegie Mellon University
Adjoint Functional Programming
We introduce some fundamental notions from proof theory, like cut elimination, polarity, focusing, and linearity and relate them throughout to advanced concepts in modern programming languages. We study their fundamental theoretical properties and explore their consequences through an implementation.
Software
To solve programming exercises and experiment with the concepts, the students should install an implementation of Standard ML (either MLton or SML/NJ ). We will provide an implementation of a small programming language in SML shortly before the summer school starts.
Lecture 1 Video | Student Notes
Lecture 2 Video | Student Notes
Lecture 3 Video | Student Notes
Lecture 4 Video | Student Notes
Lecture 5 Video | Student Notes
Alexandra Silva — Cornell University
Program Analysis with Kleene Algebra with Tests
Kleene algebra with tests is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. In these lectures, we will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for program verification, including successful extensions and fundamental limitations.
Lecture 1 Video | Student Notes
Lecture 2 Video | Student Notes
Lecture 3 Video | Student Notes
Lecture 4 Video | Student Notes
Alley Stoughton — Boston University
The Real/Ideal Paradigm
These lectures will introduce participants to the real/ideal paradigm of theoretical cryptography, which is also known as simulation-based security. We will focus on how the security of cryptographic protocols and schemes can be proved using the EasyCrypt proof assistant. But we will also consider how the real/ideal paradigm can be applied to programs whose security is enforced through programming language abstractions.
In exercises, students will be using the EasyCrypt proof assistant (see the installation instructions on my website ).
Lecture 1 Video | Lecture Slides | Student Notes
Lecture 2 Video | Lecture Slides | Student Notes
Lecture 3 Video | Lecture Slides | Student Notes
Lecture 4 Video | Lecture Slides | Student Notes
Serdar Tasiran — AWS
Getting Storage Services Right at Amazon Web Services
Storage is one of the core web services, and Amazon S3 is a widely used storage service of extreme scale. It holds Exabytes of data, is accessed 10s of millions of times per second, and consists of over 300 microservices (each a distributed system in its own right). Durability and consistency are key assurances for S3, and getting these right in a collection of dozens of development teams deploying new code weekly, dozens of new features released every year is a big challenge at a very large scale. In this talk, I will give an overview of these challenges and the formal techniques we have been using to tackle them, ranging from lightweight techniques to mechanized proof. We have used these techniques to successfully launch S3 strong consistency, new Rust-based storage nodes for S3, and, most recently, S3 Express One Zone, a storage class with 1/10th the latency of regional S3. I will end by highlighting some key formal methods, specification and implementation language challenges to motivate research.
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. The lectures will be accompanied by a Coq tutorial with exercises inspired by those applications.
Lecture 1 Video | Student Notes
Lecture 2 Video | Student Notes
Lecture 3 Video | Student Notes
Lecture 4 Video