Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning
summary
Type system enriches substructural resource types with a resettable timer that bounds progress through transition-system states and forces resources to reach accepting states or the program is rejected; it models infinite behaviours with lasso-based infinite specs, uses uniqueness typing (no aliasing) and a logical-relation proof to handle divergence, demonstrates examples that reject infinite-read and accept acquire/release with resets, and proves soundness but remains a theoretical system illustrated by worked examples.
AI-written summary · about
chapters (11)
- 0:00Temporal resource typing intro
- 1:45Resource usage verification
- 4:53Safety vs liveness violations
- 6:59Type-based resource solutions
- 8:22Contributions and goals
- 10:31Temporal specs as transitions
- 13:04Root cause of liveness issues
- 15:11Progressivity with timers
- 18:25Infinite usage handling
- 19:55Formal temporal specs
- 21:24Q&A