The (In)Efficiency of Interaction
summary
Compares four token-based abstract machines and proves precise time gaps: YAM (geometry of interaction) can be exponentially slower than Curien’s environment machine, while JAM and PALM are isomorphic and at most quadratically slower than Curien’s machine. Builds uniform simulations to relate machines, exhibits families of lambda terms achieving the separations, and shows a tight correspondence: non-idempotent intersection types measure YAM runtime (counting occurrences of the atomic type star), explaining the inefficiency as coming from higher-order types.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:19lambda calculus
- 1:10machines
- 3:20why
- 4:59summary
- 6:06token machines
- 7:43results
- 9:47typotic understanding
- 17:27runtime
- 19:38conclusion
related talks
18mMulti Types and Reasonable Space
36mAbstract Machines for Good
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
49m“Which Machine Am I Coding To?”
46mMore Interops, Good and Varied!
11mEnabling Composition of Kernels and Compilers
54mWhat Lies Beneath
01h 11mProgramming language memory models: Problems, solutions, and directions