Tail Modulo Async/Await
summary
Defines Destiny passing style as a calling convention that turns async tail and tail-modulo-cons calls into write-once promises so recursive calls allocate holes, refine destinies, fork async subcalls and fill futures when no holes remain. Claims fewer stacked frames and shorter future chains, provides a formal semantics with a work-in-progress simulation proof, and ships a proof‑of‑concept implementation in unsafe OCaml prototype while noting integration limits with OCaml/Flambda IR and missing source-level fork support.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:11Recursion and tail calls
- 3:00Async recursion challenges
- 5:38Tail async calls
- 7:28Destiny passing style
- 11:01Tail Modulo Constructor
- 13:30Tree traversal with forking
- 16:09Destiny API usage
- 18:56Code generation for Destinies
- 20:22Formal semantics and proofs
- 21:55OCaml implementation
- 22:17Q&A
related talks
21mTail Modulo Cons, OCaml, and Relational Separation Logic
20mA Tail of TwoTails: The Second Act
27mTail Recursion Modulo Context: An Equational Approach
18mHigher-order fork, modally
14mDestination calculus: A linear λ-calculus for purely functional memory writes
37mTCO
22mEfficient OCaml compilation with Flambda 2
01h 20mCoroutines for Dummies