From 7f2ddf56699c717bb7e91b745f9a0e7332fc064d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 12 Feb 2025 20:40:30 +0100 Subject: [PATCH] fix typo and add link to talk --- personal/_posts/2025-01-15-program-logics-a-la-carte.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/personal/_posts/2025-01-15-program-logics-a-la-carte.md b/personal/_posts/2025-01-15-program-logics-a-la-carte.md index 0e1c890..63041c2 100644 --- a/personal/_posts/2025-01-15-program-logics-a-la-carte.md +++ b/personal/_posts/2025-01-15-program-logics-a-la-carte.md @@ -6,8 +6,10 @@ categories: research The first paper by a PhD student I supervise has been accepted into POPL: "Program Logics à la Carte" will be presented in Denver next week. The paper proposes a framework of reusable building blocks to simplify constructing a program logic with its associated soundness proof. -This is built in Iris, and is similar to how Iris provides reusable building blocks for of the ingredients of a powerful separation logic---but so far, everything directly related to the actual language had to be re-done for each new language. +This is built in Iris, and is similar to how Iris provides reusable building blocks for the ingredients of a powerful separation logic---but so far, everything directly related to the actual language had to be re-done for each new language. By using ITrees as shared foundation, we show how this can be overcome. Congratulations, Max, on making it into POPL! To learn more, [check out the paper](https://plf.inf.ethz.ch/research/popl25-itree-program-logic.html). + +**Update:** A recording of the talk is now [available online](https://www.youtube.com/watch?v=Jff0pIbj8PM&t=14362s). -- 2.39.5