Termination in Concurrency, Revisited
summary
Compares three session-typed termination disciplines by building compositional encodings of processes and types into a Vasconcelos-style baseline, formalizing judgments and derivations to transfer guarantees. Proves that the Curry–Howard (linear-logic) class is a strict subset L ⊂ W of the weight-based Deng–Sangiorgi class, gives explicit counterexamples typable by weights but rejected by linear logic, and shows how to extract the global weight function from linear-logic derivations (a delicate but constructive procedure). Techniques: continuation-passing encodings, level/weight analysis, and countermodel construction.
AI-written summary · about
chapters (14)
- 0:00Termination in concurrency
- 1:49Why termination matters
- 3:38History of termination types
- 6:47Three typable process classes
- 9:16Type system design differences
- 13:05Vasconcelos baseline system
- 13:47San Georgi weight-based
- 14:53Curry-Howard via linear logic
- 17:18Encoding processes across systems
- 21:16Formal termination guarantees
- 22:43Counterexamples San Georgi vs Curry-Howard
- 25:33Comparative study summary
- 26:59Future work and related types
- 28:07Q&A
related talks
21mA Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
21mFair Termination of Binary Sessions
54mReasoning about Progress of Concurrent Objects
24mA Compositional Theory of Linearizability
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
01h 01mThe Future of Concurrency and Parallelism