Laura's talk details

content/lsd-seminar/2024wi.md

@@ -89,11 +89,11 @@ We present Shimmer, an all-userspace shim layer that enables host-device coordin
 
 **Speaker:** Laura Israel
 
-**Title:** _TBD_
+**Title:** The Persistence of Past: A Demand Semantics for Mechanized Cost Analysis of Lazy Programs
 
-**Abstract:** _TBD_
+**Abstract:** 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. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to formally prove that Okasaki's banker's queue is both amortized and persistent using the Coq theorem prover. We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.
 
-**Bio:** _TBD_
+**Bio:** Laura Israel is a first-year doctoral student at Portland State University studying formal verification with Yao Li. She has a particular interest in complexity theory and its formalization in proof assistants. Laura developed a passing interest in theoretical CS while getting her BA in Psychology at Reed College, resulting in a stint in the tech industry, then culminating in her current research at PSU. When she's not doing math thinly-veiled as computer science, you can find her hanging out with her cat Socks, running Dungeons and Dragons, or writing (and occasionally publishing) short stories.
 
 # Feb. 23