Synth∀ Instruction-Centric Microarchitectural Side Channel Mitigations
Speaker: Alexandra Michael
Alexandra Michael is a fourth-year PhD student and NSF GRFP recipient at the University of Washington, advised by Dan Grossman and David Kohlbrenner. Alexandra's research focuses on using formal methods to precisely specify and build verifiable solutions to challenges in hardware security, particularly around hardware side channels. She is interested broadly in using formal methods to provide sound security guarantees, including in emerging spaces like agentic security.
Abstract
As hardware manufacturers increasingly build novel microarchitectural optimizations into their chips, these optimizations often create exploitable side channel vulnerabilities. Yet the availability of defenses has not kept pace. Both hardware- and software-level mitigations take time and expertise to develop—time in which a vulnerability remains open, and expertise that may not always be readily available. We address these challenges by (1) defining a lightweight formalism for specifying instruction-centric leakage semantics; and (2) ingesting such specifications into a custom program synthesis toolchain that automatically generates transforms for a dynamic set of instructions and leakage semantics.
We present Synth∀, a framework for taking user-defined leakage semantics and using them to generate non-leaky transformations for target x86 instructions. Synth∀ combines traditional program synthesis and superoptimization tools to provide provably safe and correct program transformations. We evaluate Synth∀ on an abstract x86_64 CPU implementing a broad set of computation simplification optimizations.
What Semantics Am I This Time?: Lazy Cost Analysis is Functional Logic Programming
Speaker: Nicholas Coltharp
Nicholas Coltharp is a PhD student at Portland State University advised by Yao Li.
Abstract
Lazy evaluation enables an expressive programming style, but its non-compositional semantics makes reasoning about performance difficult. Recently, several alternative semantics have been proposed to ameliorate this problem, including clairvoyant call-by-value and demand semantics. These semantics demand tradeoffs: clairvoyant call-by-value is conceptually simple but effectively non-executable, while demand semantics is executable but conceptually complex. But it turns out that they are two sides of the same coin: using functional logic programming, we can write a single term that can simulate either semantics depending on how it is used. Thus, we need only write the same term once to get the benefits of both perspectives.
Don’t Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees
Speaker: Yiming Lin
Yiming Lin is a PhD student at Portland State University advised by Yao Li.
Abstract
Verifying existing software is hard: Programs are developed in languages not amenable to verification, involve complicated optimizations that obscure the underlying logic, and are gigantic in size. In this paper, we propose a way to ease this pain via a simplification framework that employs interaction trees as a language-agnostic interface. We show that local variable lifting, the technique underlying AutoCorres for the Simpl language, can be generalized to interaction trees via an implementation in Rocq. A key challenge with simplifying interaction trees is that they are highly dynamic structures and we would like our approach to work with mostly uninterpreted trees. We address this challenge via metaprogramming. Our metaprogramming framework is semi-automatic and proof-guided, i.e., we obtain the simplified code via a constructive proof of equivalence that can be automated via proof tactics, by utilizing Rocq’s Derive extension. This approach gives us simplified code and the equivalence theorem in one step. We demonstrate that our approach is practical using examples inspired by real-world applications.
A Taxonomy of Hoare-Like Logics
Speaker: Yao Li
Yao Li (He/Him) is an assistant professor of computer science at Portland State University. His main research area is in functional programming, interactive theorem proving, and program verification. His current research focuses on using interactive theorem provers to verify existing programs written without verification in mind. He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich.
Abstract
In this talk, I will present a paper I recently read and really liked. The paper is "A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests" (https://doi.org/10.1145/3704896). I have always been interested in incorrectness logic, but at the same time, I find it counterintuitive in a few ways; and it puzzles me whether incorrectness is indeed a dual of Hoare logic. This paper presents a very simple and clean framework for considering all these---in fact, it goes further by identifying 8 different kinds of predicate transformers and 16 different Hoare-like logics built upon them. I will discuss this framework in my talk.
Exploring comonads in Haskell
Speaker: Katie Casamento
I'm a PhD student at PSU currently working on automatically deriving decision procedures from dependent datatype definitions in Agda. In my recent free time I've been truckin' and taping Arduinos to sim racing hardware.
Abstract
In this informal guided discussion we'll explore the Comonad typeclass in Haskell as an idiom for structuring programs. Although it's rarely the most immediately practical way to solve a problem, a comonadic presentation highlights the structure of some problems in a unique way, revealing structural similarities between a variety of concepts including cellular automata and coinductive streams. If time permits we'll also explore free comonads and their relationship to free monads: in particular, over a given functor which encodes the syntax of a language, the free comonad is a type of programs and the free monad is a type of interpreters which consume those programs.
Past Terms
Winter 2026— organized by Nicholas Coltharp and Yiming Lin(7 seminars)
Fall 2025— organized by Nicholas Coltharp(4 seminars)
Spring 2025— organized by Laura Israel and Nicholas Coltharp(4 seminars)
Winter 2025— organized by Ian Kariniemi and Laura Israel(8 seminars)
Fall 2024— organized by Nicholas Coltharp and Ian Kariniemi(6 seminars)
Summer 2024— organized by Grant VanDomelen and Nicholas Coltharp(6 seminars)
Spring 2024— organized by Laura Israel and Grant VanDomelen(6 seminars)
Winter 2024— organized by Laura Israel(5 seminars)