]> git.ralfj.de Git - web.git/blobdiff - personal/_posts/2025-01-15-program-logics-a-la-carte.md
retitle MiniRust blog post
[web.git] / personal / _posts / 2025-01-15-program-logics-a-la-carte.md
index 0f1a6debede8e4e0fa230f8d3635055f8bef79de..63041c293f01638c96264dc93c5f31d4de57d315 100644 (file)
@@ -3,11 +3,13 @@ title: "Program Logics à la Carte"
 categories: research
 ---
 
 categories: research
 ---
 
-My first PhD student paper has been accepted into POPL:
+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.
 "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.
 
 By using ITrees as shared foundation, we show how this can be overcome.
 
-This is Max's first paper with me; congratulations on making it into POPL!
+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).
 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).