Type Universes as Kripke Worlds

on YouTube ↗26m

" summary

Paper claims that stratifying allocated types into a type universe hierarchy (each universe ↔ a semantic Kripke world per universe) removes the usual type–world circularity for a large class of mutable references, letting the semantics distinguish past-quantifying (predicative) from future-quantifying (impredicative/higher-order) allocations. It gives a syntax with kinding, a semantics that resembles regions, implements leveled possible-world relations, proves termination for the fragment, and characterizes which cyclic references are disallowed.

AI-written summary · about

" chapters (17)

1. 0:00Higher order mutable state
2. 2:31Possible worlds for mutable refs
3. 4:58Functions in possible worlds
4. 7:05Higher order state circularity
5. 9:55Type universes for allocations
6. 13:27Type universe hierarchy
7. 15:35Semantic equations
8. 16:38Recap: type universes & termination
9. 17:21Q&A: disallowed programs
10. 18:24Termination proof
11. 19:08Closure conversion relation
12. 20:34Termination with higher order refs
13. 21:15Separation logic comparison
14. 21:57Step indexing vs type universes
15. 23:21Propositions hierarchy & related work
16. 24:02Branching timelines & type levels
17. 25:27Polymorphism & future work