Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

Explore a groundbreaking linear concurrent separation logic called LinearActris in this 20-minute video presentation from POPL 2024. Delve into how LinearActris guarantees deadlock and leak freedom for message-passing concurrency by combining session types and concurrent separation logic. Learn about the verification of complex higher-order programs with mutable state through dependent protocols. Discover the challenges in proving the adequacy theorem of LinearActris and how a step-indexed model of separation logic based on connectivity graphs addresses this. Examine the demonstration of LinearActris's expressive power through the proof of soundness for a higher-order (GV-style) session type system using logical relations. Gain insights into the complete mechanization of results and examples in Coq, showcasing the practical applicability of this innovative approach to concurrent programming verification.