Fall 2024 Seminars

Fall 2024

Organizers: Nicholas Coltharp, Ian Kariniemi

All Talks

Date Title Speaker
Correctly Compiling Proofs Without Proving Compilers Correct Audrey Seo
Foundationally Verified Intermediate Verification Language Josh Cohen
On Extensibility J. Garrett Morris
Omnisemantics: Smooth Handling of Nondeterminism Samuel Gruetter
A breadth-first survey of Haskell terminology Katie Casamento
An introduction to Nix Nicholas Coltharp

Correctly Compiling Proofs Without Proving Compilers Correct

Speaker: Audrey Seo

Audrey Seo is a 5th year PhD student, advised by Dan Grossman, in the PLSE lab at the University of Washington. Their work falls mainly in formal methods and verification, though they are also interested in the engineering challenges of working with interactive theorem provers.

Guaranteeing correct compilation is nearly synonymous with compiler verification. However, the correctness guarantees for certified compilers and translation validation can be stronger than we need. While many compilers do have incorrect behavior, even when a compiler bug occurs, it may not change the program’s behavior meaningfully with respect to its specification. In this talk, I will explain our technique for getting strong guarantees about compiled programs even in the presence of unverified or even incorrect compilers. Our workflow compiles programs, specifications, and proof objects, from an embedded source language and logic to an embedded target language and logic. Our source and target languages are simple and imperative, and each has its own Hoare-style program logic. We are able to use our workflow with multiple different compilers -- all with varying degrees of correctness -- to successfully compile Hoare proofs about source programs to equivalent Hoare proofs about target programs. All results are formalized and proven correct in the proof assistant Rocq, formerly known as Coq. This opens up new options for which proof burdens one might shoulder instead of, or in addition to, compiler correctness.

Foundationally Verified Intermediate Verification Language

Speaker: Josh Cohen

Josh Cohen is a final-year PhD student at Princeton advised by Andrew Appel. His research focuses on foundationally sound program verification, particularly ways of combining automated and interactive proof methods to make program verification easier without sacrificing foundational guarantees. Previously, he received his Bachelor's degree in math and computer science from the University of Pennsylvania.

Annotation-based deductive verifiers have emerged in recent years as practical, capable, and increasingly scalable tools for verifying programs in languages including C, Rust, Go, OCaml, and Dafny. Their proliferation is largely thanks to Intermediate Verification Languages (IVLs) such as Why3, Boogie, and Viper, which greatly reduce the difficulty of building such tools by performing some of the difficult translations from high-level, expressive program logics to SMT. But these verifiers are difficult to fully trust: their toolchains comprise hundreds of thousands to millions of lines of code and bugs in any part can result in unsoundness. An alternate approach to building program verifiers is the foundational one, where the language semantics, program logic, and user-supplied proofs are defined in a proof assistant, giving an end-to-end soundness theorem. Such tools, including VST, CakeML, and Bedrock2, provide very strong guarantees but have a high barrier to entry. These two approaches have largely remained separate. IVL tools are not themselves verified, while fully verified tools cannot take advantage of the automation provided by the IVL and SMT-based pipelines. In this talk, I will describe our efforts to bridge this gap by providing an implementation of the Why3 IVL in the Coq proof assistant, giving the first foundationally verified IVL implementation. First, we give a novel formal semantics for a core subset of the logic implemented by Why3 - polymorphic first-order logic with recursive types, functions, and predicates. We then develop a new framework to idiomatically implement OCaml APIs in Coq and use this to produce a Coq implementation of the Why3 logic API and transformations. Finally, we prove the correctness of our implementation against our formal semantics; we give the first machine-checked soundness proofs for several of the transformations used to compile Why3's logic to SMT.

On Extensibility

Speaker: J. Garrett Morris

J. Garrett Morris is an assistant professor and the inaugural Emeriti Faculty Scholar in the Department of Computer Science at the University of Iowa. He received his Ph.D. from Portland State University in Oregon, and post-doctoral training at the University of Edinburgh, Scotland. His research focuses on the development of type systems for higher-order functional programming languages, with the twin aims of improving expressiveness and modularity in high-level programming and supporting safe concurrent, low-level, and effectful programming. His work has appeared in top venues in programming language theory and functional programming, and is supported by NSF.

This talk will present some recent results on modularity and extensible data types. My research into programming languages and their type systems is guided by two overarching goals. On the one hand, types should precisely specify program behavior, allowing programmers to rule out classes of erroneous behavior. On the other, types should enable expressive tools, allowing programmers to build modular, re-usable software and software components. My work inhabits the intersection of these ideas, refining generic programming mechanisms both to better enforce intended program behavior and to support more expressive abstractions. Extensibility is an evergreen problem in programming and programming language design. The goal is simple: specifications of programs and their data should support the addition of both new kinds of data and new operations on data. Despite this problem having been identified as early as 1975, modern languages lack effective solutions. Object-oriented languages require programmers to adopt unintuitive patterns like visitors, while functional languages rely on encodings of data types. Lower-level languages, where similar problems arise, rely on textual substitution. I will present recent work which proposes a unified approach to extensible data and program specification. I will show how this work both encompasses existing approaches to extensible data types and captures examples inexpressible in all existing systems. Our approach naturally generalizes, supporting powerful label-generic operations, and pointing toward expressive encodings of extensible recursive functions.

Omnisemantics: Smooth Handling of Nondeterminism

Speaker: Samuel Gruetter

Samuel Gruetter is a postdoc in Timothy (Mothy) Roscoe’s group at ETH Zurich. He did his PhD in Computer Science at MIT in Adam Chlipala's group, working on formal verification of software using the Coq proof assistant. Prior to MIT, Samuel received a Bachelor's and Master's at EPFL in Lausanne, where he was a student research assistant in Martin Odersky's Scala lab, working on the theoretical foundations of the Scala language. He did a Master's project internship at Princeton University with Andrew Appel's group, working on their Verified Software Toolchain, and also worked at the University of Melbourne, Australia, with Toby Murray on information flow proofs for C programs.

When working with traditional small-step or big-step operational semantics, modeling undefined behavior as absence of any transition is convenient for proofs like compiler correctness or type safety. However, once we add nondeterminism, expressing and proving absence of undefined behavior becomes cumbersome, because we have to make sure we don’t forget about nondeterministic branches that get stuck at some point. Using a new style of semantics that we call omnisemantics, where one derivation talks about all possible executions, we get a concise way of expressing absence of undefined behavior that enables convenient proofs by induction, including forward-simulation compiler correctness proofs rather than the much harder-to-write backwards-simulation proofs. Related paper [TOPLAS’23]: https://dl.acm.org/doi/10.1145/3579834

A breadth-first survey of Haskell terminology

Speaker: Katie Casamento

Everyone who learns Haskell (or interacts with Haskell people) encounters quite a few vocabulary terms that are likely to be brand new to them: not just the commonly-discussed Functor/Applicative/Monad hierarchy, but the Foldable/Traversable hierarchy, the Generic/Generic1 hierarchy, several Functor variations, and in modern Haskell code often the Optic hierarchy as well. While each of these topics is worthy of deep study individually, it is a misconception that deep study of each individual concept is required in order to make practical use of the tools in this toolbox. My goal in this session is to guide a practically-focused discussion on the vocabulary of modern Haskell, without getting too caught up in the theory of each of these concepts. Ultimately, I hope that everyone will come away feeling more confident in their ability to follow and participate in conversations with Haskell people.

An introduction to Nix

Speaker: Nicholas Coltharp

Nix is a functional system for software deployment that has gained a lot of traction in PL-adjacent communities. This talk will be an introduction to Nix: the basics of how it works and what it can do for you.