Reasoning about Laziness is Reasoning about Future: Alternative Semantics to Lazy Evaluation
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Classical works often rely on either reasoning about mutable heaps or modeling sharing via explicit combinators. In this talk, I focus on a different approach: we use alternative semantics that are equivalent to lazy evaluation but more amenable to formal reasoning. I will talk about two such alternative semantics: a clairvoyant semantics based on Hackett & Hutton (2019) and a demand semantics based on Bjerner & Holmström (1989). We show how we can use these semantics to mechanically reason about computation cost of lazy functions using the Rocq Prover (formerly known as the Coq theorem prover).

Bio: 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. Some of his past work includes the verification of the DeepSpec web server and the verification of Haskell's containers library (using hs-to-coq). He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich. Before that, he obtained a MS degree and a BS degree from Shanghai Jiao Tong University in 2016 and 2013, respectively.