]> git.ralfj.de Git - web.git/blobdiff - personal/_posts/2025-01-15-program-logics-a-la-carte.md
try to make the wording less confusing
[web.git] / personal / _posts / 2025-01-15-program-logics-a-la-carte.md
index 0f1a6debede8e4e0fa230f8d3635055f8bef79de..0e1c890bcece1e5f581b5bcda1674d1db022b7e6 100644 (file)
@@ -3,11 +3,11 @@ 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.
 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.
 By using ITrees as shared foundation, we show how this can be overcome.
 
 "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.
 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).