Formal Foundations for Programs with Interacting Effects

ABSTRACT

Critical software components often display effects such as randomization, nondeterminism, concurrency, and exceptions. Complex combinations of effects show up in distributed systems, security, and privacy applications where correctness is crucial, but mixtures of effects also make testing and informal reasoning difficult or impossible. While powerful formal methods exist for verifying programs with individual effects, those approaches do not provide a unified account of how such effects interact. As a result, verification techniques are highly specialized and difficult to compose.

In this talk, I present Outcome Logic, a logical foundation that captures diverse program behaviors via a common notion of outcomes. Outcome Logic enables reusable reasoning principles across deterministic, nondeterministic, and probabilistic settings, and allows multiple effects to be composed on top of the base logic. I will show how the extensible approach allows Outcome Logic to support new types of reasoning in domains such as verification of randomized distributed systems and principled bug-finding techniques,

BIOGRAPHY

Noam is a final year PhD Candidate at Cornell University in the area of Programming Languages and Formal Methods, advised by Alexandra Silva. Before coming to Cornell, he was a staff software engineer in the Facebook Programming Languages and Runtimes team, where he led development of type system features for the Hack programming language and formally verified concurrent algorithms for an OS microkernel. Noam's current research focuses on logical foundations for reasoning about programs that branch into different outcomes, which provide a unifying perspective for reasoning about a wide variety of effects including nondeterminism, nontermination, randomization, concurrency, and exceptions. The resulting Outcome Logic has applications in automated bug-finding and verification of concurrent randomized algorithms. Noam's research is supported in part by an NSF Medium award and he was recently recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software research and a distinguished paper award at POPL 2026.