PL Meets Verification on October 22, 2025

Presenter: Jianlin Li Abstract: We present a new approach to scaling exact inference for probabilistic programs, using generating functions (GFs) as a compilation target. Existing methods that target representations like binary decision diagrams (BDDs) achieve strong state-of-the-art results.

Presenter: Yizhou Zhang Abstract: This talk shares how ideas from object-oriented programming can help us rethink the way we write and organize machine-checked proofs—and how different paradigms can come together in surprising ways.

Presenter: Cong Ma Abstract: Effect handlers are a powerful feature for structuring programs with rich control flow. Lexical effect handlers, in particular, offer better modularity and stronger reasoning principles. In this talk, I’ll introduce effect handlers and share our work on Lexa, a language and compiler built to compile lexical handlers efficiently and correctly.

Presenter: Shenghua Feng Abstract: In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds.