A Lightweight Type-and-Effect System for Invalidation Safety - Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype Inference

Explore a 14-minute conference presentation from OOPSLA 2025 that introduces InvalML, a novel type-and-effect system designed to address invalidation safety in programming languages. Learn how researchers Cunyuan Gao and Lionel Parreaux from Hong Kong University of Science and Technology developed a higher-rank polymorphic system that statically tracks both permanent and temporary invalidation of sensitive values and resources without imposing aliasing or capture restrictions. Discover how this system uses Boolean-algebraic types including unions, intersections, and negations to precisely model side effects and guarantee invalidation safety across various programming scenarios. Understand the practical type inference algorithm that requires minimal programmer annotations, focusing only on higher-rank and polymorphically-recursive functions. Examine the wide-ranging applications of this approach, including stack-based and region-based memory management, iterator invalidation prevention, data-race-free concurrency, mutable state encapsulation, type-safe exception and effect handlers, and scope-safe metaprogramming. Gain insights into how this lightweight solution overcomes limitations of previous approaches that restricted language expressiveness while providing robust safety guarantees for resource management and program correctness.