A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
summary
A new system named InvalML statically tracks both permanent and temporary invalidation for regioned resources by combining Boolean-algebraic types (unions intersections negation) with higher-rank polymorphism and a constraint solver that integrates subtype solving and bidirectional checking. It introduces outer variables to abstract unknown surrounding regions and uses constraint-based subtype inference so programmers only annotate higher-rank or polymorphically recursive functions. The paper ships a complete inference algorithm plus artifacts that reproduce evaluation and show the system accepts iterator-and-region patterns rejected by linear/unique approaches.
AI-written summary · about
chapters (11)
- 0:00Invalidation safety intro
- 1:21Motivating example with regions
- 2:25Limitations of linear types
- 3:29Boolean subtyping and effects
- 4:55Permanent vs temporary invalidation
- 5:59Region-based type variables
- 7:24Effect constraints for safety
- 8:49Nested regions and polymorphism
- 10:36Unknown region variables
- 10:58Summary of contributions
- 11:39Question and answer session
related talks
15mKindly Bent to Free Us
21mPractical Type Inference with Levels
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
21mLazy Validation and Self-Healing for Agentic Programs
30mAutomatic Inference of Relational Object Invariants
33mResource polymorphism: proposal for integrating first-class resources into ML
19mPete's Footprints
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)