Soundly Handling Linearity - Combining Linear Types with Multi-Shot Effect Handlers

Explore a novel approach to combining linear types with multi-shot effect handlers in this 16-minute video presentation from POPL 2024. Delve into the concept of control-flow linearity as a solution to soundness issues in systems that mix linearity with effect handlers. Examine the formalization of this approach in a System F-style core calculus called Feff∘, featuring linear types, an effect type system, and effect handlers. Learn about the linearity-aware semantics used to prove the preservation of linear value integrity. Discover how this approach has been adapted to fix a long-standing soundness bug in the Links programming language. Explore the potential of control-flow linearity through the introduction of Qeff∘, an ML-style core calculus that uses qualified types for type inference without programmer annotations. Gain insights into overcoming practical limitations, including abstraction over linearity, linearity dependencies between type variables, and fine-grained control-flow linearity.

[POPL'24] Soundly Handling Linearity