X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/e9402f62f987e4b38dc29ba7ddceb9a3ff049f53..cbf690bdc20376d9f620cab580985add85c2e7a0:/personal/_posts/2025-01-15-program-logics-a-la-carte.md

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
new file mode 100644
index 0000000..0f1a6de
--- /dev/null
+++ b/personal/_posts/2025-01-15-program-logics-a-la-carte.md
@@ -0,0 +1,13 @@
+---
+title: "Program Logics à la Carte"
+categories: research
+---
+
+My first PhD student paper 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.
+
+This is Max's first paper with me; congratulations on making it into POPL!
+To learn more, [check out the paper](https://plf.inf.ethz.ch/research/popl25-itree-program-logic.html).