# POP

Probabilistic couplings are a standard mathematical abstraction for reasoning about two distributions. In formal verification, they are often called probabilistic liftings. While these two concepts are quite related, the connection has been little explored. In fact, probabilistic couplings and liftings are a powerful, compositional tool for reasoning about probabilistic programs. I will give a brief survey of different uses of probabilistic liftings, and then show how to use these ideas in the relational program logic pRHL.

*Joint with Gilles Barthe, Thomas Espitau, Benjamin Gregoire, and Pierre-Yves Strub.*

—

Justin Hsu is a final year graduate student at the University of Pennsylvania, advised by Benjamin Pierce and Aaron Roth. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.

**Faculty Host:** Matt Fredrikson

It's tempting to think that machine instructions are atomic updates to a global mutable state, of register and memory values. In the sequential world that's a good model, but concurrent contexts expose a slew of more interesting behaviour. We set out to understand real multiprocessor semantics in 2007, to give a basis for software verification. We're still not done, but we now have credible operational models for much of what goes on. I'll talk about some key points of this, including our experimental investigation and validation, the Lem and Sail metalanguages for expressing the semantics, our interactions with processor vendors, especially IBM and ARM, and work with the CHERI team on secure hardware and software. It's impacted hardware testing, architecture design, and high-level language design along the way.

This is part of the REMS project, aiming to apply semantics to improve the quality of mainstream computer systems; REMS also includes work on the C language and C/C++ concurrency model, on ELF linking, on POSIX filesystems, on the TCP and TLS network and security protocols, on the CakeML verified compiler, and on program logics. I'll start with a quick overview of REMS.

*This is joint work with Shaked Flur, Susmit Sarkar, Kathryn E. Gray, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Ali Sezgin, Gabriel Kerneis, Dominic Mulligan, Anthony Fox, Robert Norton-Wright.*

—

Peter Sewell is a Professor of Computer Science at the University of Cambridge Computer Laboratory. He held an EPSRC Leadership Fellowship from 2010-2014 and a Royal Society University Research Fellowship from 1999-2007; he took his PhD in Edinburgh in 1995, supervised by Robin Milner, after studying in Cambridge and Oxford. His research aims to build rigorous foundations for the engineering of real-world computer systems, to make them better-understood, more robust, and more secure.

**Faculty Host:** Robert Harper

Rust is a new systems-programming language that is becoming increasingly popular. It aims to combine C++'s focus on zero-cost abstractions with numerous ideas that emerged first in academia, most notably affine and region types ("ownership and borrowing") and Haskell's type classes ("traits"). One of the key goals for Rust is that it does not require a garbage collector.

In this talk, I'll give a brief overview of Rust's key features, with a focus on the type system. I'll talk about how we leverage a few core features to offer a variety of APIs -- ranging from efficient collections to various styles of parallel programming -- while still guaranteeing memory safety and data-race freedom.

—

Nicholas Matsakis is a senior researcher at Mozilla research and a member of the Rust core team. He has been working on Rust for four years and did much of the initial work on its type system and other core features. He has also done work in several just-in-time compilers as well as building high-performance networking systems. He did his undergraduate study at MIT, graduating in 2001, and later obtained a PhD in 2011, working with Thomas Gross at ETH Zurich.

**Faculty Host:** Stephanie Balzer

In this talk I will present Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and an internal notion of a cursor. Existing structure editors only guarantee a weak syntactic well-formedness. Hazelnut goes one step further: the possible edit actions maintain static well-definedness. Naively, this prohibition on ill-typed edit states would force the programmer to construct terms in a rigid outside-in manner. To avoid this problem, the semantics of edit actions automatically places terms assigned a type that is inconsistent with the expected type inside a hole. This safely defers the type consistency check until the programmer finishes constructing the term inside the hole.

Hazelnut is a foundational type-theoretic account of typed structure editing, rather than an end-user tool itself. To that end, I will describe how Hazelnut's rich metatheory, which is fully mechanized in Agda, guides the definition of an extension to the calculus. I will also discuss future work considering plausible evaluation strategies for terms with holes, and reveal connections with gradual typing and contextual modal type theory. Finally, I will discuss how Hazelnut's semantics lends itself to implementation as a functional reactive program in js_of_ocaml.

*Hazelnut is joint work with Cyrus Omar, Michael Hilton, Jonathan Aldrich, and Matthew Hammer.*

*—*

Ian Voysey received his Bachelor's degree in Computer Science and Discrete Mathematics and Logic from Carnegie Mellon University in 2010. He helped to develop the introductory functional programming courses there, and won the inaugural A. Nico Habermann Educational Service Award for that work. His research interests are in mechanized proof, proof theory, and type theory. He is currently a Research Programmer at Carnegie Mellon University.

**Faculty Host:** Jonathan Aldrich

Software has become a central and integral part of many systems and products of the information era. In embedded and cyber-physical systems, software is not an isolated component but instead an integrated part of larger, e.g. technical or mechanical systems. During the last decade, there has been an exponential growth in the size of embedded software, resulting in an increasing need for software engineering methods addressing the special needs of the embedded and cyber-physical domain.

In this talk, I discuss the challenges that arise in the field of software engineering in embedded and cyber-physical systems. Since such systems are often used in safety- and security-critical environments, it is an urgent problem how their reliability and correctness can be ensured. A particular problem arises due to the hybrid nature of these systems as they contain both discrete and continuous parts that interact together. I demonstrate how these requirements can be met by presenting some of our research results from the automotive domain and from hardware/software co-design and co-verification. Concludingly, I give an overview over further research topics in my group.

—

Prof. Dr. Sabine Glesner is a full professor at the Technical University of Berlin, heading the chair Software and Embedded Systems Engineering. Dr. Glesner holds a Master of Science in Computer Science from the University of California, Berkeley, a diploma degree in Computer Science from the Technical University of Darmstadt, Germany, and a Ph.D. in Computer Science from the University of Karlsruhe, Germany. At the University of Karlsruhe, she also finished her habilitation, which qualified her as a university teacher. Dr. Glesner's research lies in the fields of software engineering, embedded systems, and hardware/software co-design, with a particular focus on validation and verification. Her research projects have been funded, among others, by the German Research Foundation (DFG), the European Commission, and the Federal Ministry for Education and Research.

**Faculty Host: ** André Platzer

Julia is a relatively new language gaining popularity in technical computing and data analysis fields. It began as an attempt to understand the appeal of languages like Matlab, R, and Python/NumPy at a fundamental level, and to ask how they can be improved. We arrived at a design based on subtyping and multiple dispatch that provides a good tradeoff between performance and productivity for many users. This talk will discuss some of Julia's more novel features, particularly its subtyping and method system, and some possible future directions.

—

Jeff Bezanson is one of the creators of the Julia language, beginning at MIT in 2009 along with Alan Edelman, Stefan Karpinski, and Viral Shah. He received a PhD from MIT in 2015 and is now a co-founder of Julia Computing, Inc. which provides consulting and commercial support around the language. Before the Julia project, Jeff worked as a software engineer on compilers and in the areas of parallel and scientific computing.

**Faculty Host:** Jean Yang

Trading in financial markets is a data-driven affair, and as such, it requires applications that can efficiently filter, transform and present data to users in real time.

But there's a difficult problem at the heart of building such applications: finding a way of expressing the necessary transformations of the data in a way that is simultaneously easy to understand and efficient to execute over large streams of data.

This talk will show how we've approached this problem using /Incremental/, an OCaml library for constructing dynamic computations that update efficiently in response to changing data. We'll show how Incremental can be used throughout the application, from the servers providing the data to be visualized, to the JavaScript code that generates DOM nodes in the browser. We'll also discuss how these applications have driven us to develop ways of using efficiently diffable data structures to bridge the worlds of functional and incremental computing.

—

Yaron Minsky obtained his BA in mathematics from Princeton University and his PhD in Computer Science from Cornell University, focusing on distributed systems. In 2003, he joined Jane Street where he has worked in a number of areas, founding the quantitative research group and helping transition the firm to using OCaml, a statically typed functional programming langauge, as its primary development platform.

**Facult Host:** Jan Hoffmann

AUTO2 is a new heuristic theorem prover written for the proof assistant Isabelle. It uses a robust search mechanism that bears some similarity to those used in SMT solvers. On the other hand, it retains several advantages of the tactics framework in Isabelle, such as allowing custom procedures and working with higher-order logic. In this talk, I will discuss the ideas behind auto2 and show some examples of its use in various parts of mathematics and computer science. In the end I will also discuss the more recent application to automation in separation logic.

—

Bohua Zhan is a postdoc in the department of mathematics at MIT, currently working on automation techniques in interactive theorem provers. Previously I worked in low-dimensional topology, receiving my PhD in mathematics from Princeton, under the supervision of Zoltan Szabo.

**Faculty Host:** Jeremy Avigad

The λΠ-calculus modulo theory, implemented in the Dedukti system, is a logical framework where many theories can be expressed: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes... This allows to use it to check large libraries of proofs coming from various proofsystems: Zenon, iProver, FoCaLiZe, HOL-Light, and Matita.

—

Olivier Hermant is an associate researcher at MINES ParisTech, on a sabbatical leave at Wesleyan University. He got his PhD in 2005, under the supervision of Gilles Dowek, and his research interests are the combination of rewriting and proof systems, automated theorem proving, semantics and completeness theorems, and type systems.

**Faculty Host:** Robert Harper

In recent years, Boolean Satisfiability (SAT) solvers have been successfully used in many practical applications. Given a propositional formula, the SAT problem consists in deciding if the formula is satisfiable or unsatisfiable. For unsatisfiable formulas, we are often interested in knowing what is the maximum number of clauses that can be simultaneously satisfied. Such problem is known as the Maximum Satisfiability (MaxSAT) problem, the optimization counterpart to SAT as a decision problem. Many real-world applications, such as software package upgrades, error localization in C code, and malware detection, can be encoded into MaxSAT and take advantage of the recent advances in MaxSAT solving.

In this talk, I will present effective and novel MaxSAT algorithms that lead to an order of magnitude improvement for solving real-world problems. I will also survey applications of MaxSAT, focusing on Android malware detection. Specifically, I will explain how to automatically infer malware signatures using MaxSAT from very few samples of a malware family with an accuracy of over 90%.

—

Ruben Martins is a postdoctoral researcher at the University of Texas at Austin, USA. Prior to joining UT Austin, he was a postdoctoral researcher at the University of Oxford, UK, and he received his PhD with honors from the Technical University of Lisbon, Portugal in 2013. His research aims to improve constraint solvers and broaden their applicability in program analysis, synthesis, and security. Dr. Martins has developed several award winning solvers and has consistently improved the state-of-the-art in Maximum Satisfiability (MaxSAT)< solving. He is currently the main developer of Open-WBO: an open source MaxSAT solver that won several awards in the MaxSAT competitions.

**Faculty Host:** Frank Pfenning