The Logical Essence of Well-Bracketed Control Flow

Explore a 19-minute video presentation from POPL 2024 conference that delves into the logical essence of well-bracketed control flow in programming. Learn about a novel Hoare-style program logic based on separation logic for reasoning about well-bracketedness. Discover how this approach can be used to demonstrate correctness of well-bracketed programs through direct methods and by defining unary and binary logical relations models. Understand the significance of well-bracketed control flow, where called functions must return before their callers resume execution. Gain insights into the formalization of these concepts using the Iris framework and their mechanization in the Coq proof assistant. Access supplementary materials, including reusable artifacts, to further explore the research findings presented by Amin Timany, Armaël Guéneau, and Lars Birkedal from Aarhus University and Université Paris-Saclay.

[POPL'24] The Logical Essence of Well-Bracketed Control Flow