Type Universes as Kripke Worlds: Memory Management Edition
summary
Claims a tight correspondence between dependent-type type universe hierarchy and Kripke-style heap worlds, using a kinding discipline to forbid cross-level and self-references so the semantic interpretation restricts each type to a world truncated at its level. This yields a model of higher-order state that avoids no step-indexing machinery and proves termination for the restricted fragment. Using displacement operator / universe polymorphism lets values be allocated into fresh universes so those regions can be reclaimed, but universes start out very large which limits straightforward region-style memory savings.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:45Higher order state
- 3:10Type universes hierarchy
- 5:40Circularity and simplicity
- 7:26Semantic values and heap
- 8:51Memory management limits
- 9:54Polymorphism and displacement
- 11:40Regions as universes
- 13:27Algebra of levels
- 14:31Summary
- 15:58Q&A
- 16:19Cross-universe references
- 17:00Partial orders in hierarchies
- 17:41Type and effect systems
- 18:45Inverting references
- 19:49Chaining references
- 20:51Termination and data structures
- 21:32Conclusion