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