From d196d9181010320ed5a7f89e9d5e132c715b226d Mon Sep 17 00:00:00 2001 From: lkuper Date: Mon, 12 Feb 2024 20:16:43 +0000 Subject: [PATCH] regenerate after: Laura's talk details --- index.xml | 6 +++--- lsd-seminar/2024wi/index.html | 6 +++--- themes/academic | 1 + 3 files changed, 7 insertions(+), 6 deletions(-) create mode 160000 themes/academic diff --git a/index.xml b/index.xml index 4cdda89..fff4f1c 100644 --- a/index.xml +++ b/index.xml @@ -201,11 +201,11 @@ <p><strong>Speaker:</strong> Laura Israel</p> -<p><strong>Title:</strong> <em>TBD</em></p> +<p><strong>Title:</strong> The Persistence of Past: A Demand Semantics for Mechanized Cost Analysis of Lazy Programs</p> -<p><strong>Abstract:</strong> <em>TBD</em></p> +<p><strong>Abstract:</strong> 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&rsquo;s banker&rsquo;s queue is both amortized and persistent using the Coq theorem prover. We also propose the reverse physicist&rsquo;s method, a novel variant of the classical physicist&rsquo;s method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.</p> -<p><strong>Bio:</strong> <em>TBD</em></p> +<p><strong>Bio:</strong> 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&rsquo;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.</p> <h1 id="feb-23">Feb. 23</h1> diff --git a/lsd-seminar/2024wi/index.html b/lsd-seminar/2024wi/index.html index 4d5b906..cf6fdf6 100644 --- a/lsd-seminar/2024wi/index.html +++ b/lsd-seminar/2024wi/index.html @@ -340,11 +340,11 @@

Feb. 16

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

diff --git a/themes/academic b/themes/academic new file mode 160000 index 0000000..8d596ff --- /dev/null +++ b/themes/academic @@ -0,0 +1 @@ +Subproject commit 8d596ffed2d080010c561679cf4e9b4da1554781