Mechanizing Session-Types Using a Structural View - Enforcing Linearity without Linearity

Explore a 19-minute video presentation from OOPSLA2 2023 conference that introduces a novel technique for mechanizing session types using a structural view. Learn how researchers from McGill University demonstrate a method to enforce linearity without relying on linear typing contexts, instead embedding linearity conditions as predicates within type judgments. Discover the advantages of this approach in handling channel mobility and complex binding structures in session-typed systems. Examine the mechanization of a session-typed system based on classical linear logic and its type preservation proof using the Beluga proof assistant. Gain insights into the effectiveness of this approach for modeling substructural systems like session-typed languages, supported by an adequacy proof for the encoding. Access supplementary materials, including reusable artifacts, to further understand the implementation and implications of this research in the field of concurrent programming and type systems.