Multi Types and Reasonable Space
summary
Claims a concrete machine, Space KAM, is a reasonable space cost model for the lambda calculus (linear overhead vs. Turing/RAM) and handles logarithmic-space computations. Builds a variant of intersection/multi types enriched with multiset labels — “closure types” that annotate variables with natural-number sizes — and proves soundness and completeness: the derivation weight equals the Space KAM’s maximal closure space. Also shows minor type changes capture the machine’s time cost.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:13Computational Models
- 3:07The Krivine's Abstract Machine
- 5:27Simple Types and the KAM
- 6:37Multi Types and the KAM
- 8:52On the KAM and Space Consumption
- 10:29The Space KAM
- 12:48Multi Types and the Size of Closures
- 13:32Closure Types
- 14:20Some Typing Rules
- 16:00The Main Result
- 16:23Wrapping Up
related talks
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
23mA Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
36mDependently Typed Multi-Stage Programming, Revisited
22mQuantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
21mThe (In)Efficiency of Interaction
39mA Reusable Machine-Calculus for Automated Resource Analyses
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
36mAbstract Machines for Good