Program Logics à la Carte

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.

Congratulations, Max, on making it into POPL! To learn more, check out the paper.

Posted on Ralf's Ramblings on Jan 15, 2025.
Comments? Drop me a mail!