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
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.
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.
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.
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.
Frank Pfenning — Carnegie Mellon University
Proof Theory and Programming Languages
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.
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.
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. And we will provide an introduction to a strong, modular form of the real/ideal paradigm called Universally Composable (UC) Security, considering a domain specific language (DSL) for expressing UC designs.
In exercises, students will be using the EasyCrypt proof assistant (see the installation instructions on my website ), and the implementation of the UC DSL (see the installation instructions at GitHub ).
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.