Lars Birkedal

A relational model of types-and-effects in higher-order concurrent separation logic

2016

Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating …

The Logical Essence of Well-Bracketed Control Flow

2024 · Proceedings of the ACM on Programming Languages

A program is said to be well-bracketed if every called function must return before its caller can resume execution. This is often the case. Well-bracketedness has been captured semantically as a condition on strategies in …