A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types

Explore a 21-minute conference talk from CoqPL 2025 that presents groundbreaking research on session types in concurrent systems. Learn about the development of a semantic logical relation for proving termination in Intuitionistic Linear Logic Session Types (ILLST). The presenters—Tarakaram Gollamudi, Jules Jacobs, Yue Yao, and Stephanie Balzer from Cornell University and Carnegie Mellon University—explain how they created the first mechanization of a logical relation for termination of session types using the Coq proof assistant. Discover how session types specify protocols in message-passing concurrent systems, their foundation in linear logic through Curry-Howard correspondence, and why proving termination requires special techniques when operational semantics are defined explicitly. The talk introduces ILLST, its logical relation, and a novel rooted tree dynamics, demonstrating that well-typed ILLST programs are terminating through the fundamental theorem.