A silent semantics for isorecursive session types
summary
Claim: isorecursive session types can often avoid runtime roll/unroll if all recursions are contractive isorecursive types, and an algorithm extracts adapter witnesses from a coinductive equivalence proof to mediate between equi- and iso-recursive views. Implementation: a translation that inserts adapters and preserves typing. Failure: operational correspondence breaks because adapters spawn forks that desynchronize reductions, so simple simulation fails. Conclusion: need richer reasoning—an equational theory or simulation up-to/logical relations—to recover a correctness proof.
AI-written summary · about
chapters (18)
- 0:00Welcome
- 0:26Motivation for recursive session types
- 1:53Duality problems with recursion
- 3:43Two approaches to recursion
- 6:08Equirecursion in session types
- 7:51Challenges of isorecursion
- 9:18Adapter processes for equivalence
- 12:08Witness terms for proofs
- 13:54Circular witness terms and coinduction
- 14:59Translating equirecursion to isorecursion
- 16:28Reverse translation to equirecursion
- 17:35Contractive isorecursive programs
- 18:16Simulation between equirecursion and isorecursion
- 20:46Why translation breaks reduction
- 21:55Administrative reductions and theory
- 24:03Advanced equational theories
- 24:46Open problems and future work
- 25:29Q&A