X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/bcc0673c7d883945b7b29440642998a690c44d07..5d4a889d31bb09e8732c90af9f9675ce48c7b60e:/personal/_posts/2025-01-15-program-logics-a-la-carte.md?ds=inline

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).