A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
summary
Proves termination for intuitionistic linear logic session types (ILLST) by building a semantic unary logical relation and showing the fundamental theorem: well-typed programs multi-step to a value-or-poised state. Delivers a full Coq mechanization (first of its kind), a rooted-tree configuration dynamics, concrete substitution and gmap-based implementations, and proofs that tensor/choice rules preserve the relation; includes worked examples and a clear corollary for closed unit-typed processes.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:09Session types overview
- 5:45Typing judgment
- 7:12Tensor typing rules
- 9:42Configurations and dynamics
- 11:29Mechanization details
- 12:52Logical relation
- 15:48Termination theorem
- 18:19Substitution details
- 19:23Q&A
related talks
31mTermination in Concurrency, Revisited
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
21mFair Termination of Binary Sessions
28mDependent Session Protocols in Separation Logic from First Principles
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...