What we learned from writing a book about session types
summary
A book documents a concrete development path: start from a minimal session calculus with a double-binder design, no primitive data, and mechanized-free proofs of type preservation and safety; formalize infinite session types via coinduction and finite mu-syntax; define sharable versus linear channels with a UN predicate for sharability plus explicit contraction/weakening rules; discover a safe subtyping mix between linear and unrestricted types; implement an encoding into linear types by adapting the target to double binders; leave algorithmic typechecking and mechanization as unfinished engineering work.
AI-written summary · about
chapters (14)
- 0:00Writing a book on session types
- 1:04Book project started in 2019
- 2:28Book content and sources
- 5:00Structuring the book challenges
- 6:01Building simple system first
- 8:27Proving session fidelity in binary
- 9:10Handling infinite behavior
- 10:35Adding nonlinear types
- 13:26Send-on-self debate
- 14:56Subtyping surprises
- 18:29Type checking algorithm design
- 20:17Encoding session types
- 22:07Linear logic connection choice
- 24:59Final thoughts and status
related talks
01h 00mTheory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5
20mA Core Calculus for Documents: Or, Lambda: The Ultimate Document
54mPanel: Mechanized Specifications for Real-World Programming Languages
27mProduction Language Specification - Requirements for Multiple Usages
01h 39m“Learning and Teaching Modern C++”
32mA Survey of Weak Reasoning Assistants
36mGoing Modular: Teaching Old Docs New Tricks
29mLegalese: Software Eats Contract Drafting