Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This video presents a conference talk from POPL 2025 by researchers Max Vistrup, Michael Sammler, and Ralf Jung from ETH Zurich, Switzerland, addressing the challenge of reusing program logic components across different programming languages. Learn how the researchers propose a modular approach called "Program Logics à la Carte" that enables the composition of program logic fragments for various language effects including shared state, concurrency, and non-determinism. The approach builds on Interaction Trees (ITrees) as a framework for expressing language semantics and Iris as the underlying separation logic, with the entire work mechanized in the Coq proof assistant. The 21-minute presentation demonstrates how this modular approach overcomes the current limitation where developers of new program logics must establish every part from scratch, despite programming languages sharing many core features. The research has been published in an article available at https://doi.org/10.1145/3704847, with supplementary materials that have earned "Artifacts Available" and "Artifacts Evaluated — Reusable" badges.
