Simple Reference Immutability for System F-sub
summary
Presents a formal calculus extending System F_sub with a runtime seal operator that enforces transitive reference immutability, models records as mutable references (with intersection types), and proves progress and preservation plus equivalence lemmas showing seals only cause stuckness. Shows a type-level readon qualifier with a normal form (single outer readon) so read-only-typed but unsealed references cannot be written to, provides mechanized proofs and evaluated artifacts linked from the paper.
AI-written summary · about
chapters (13)
- 0:00Reference immutability intro
- 1:01Why mutation is useful and dangerous
- 2:26What is reference immutability
- 3:48Transitive immutability with read-only refs
- 4:50Seals for runtime record protection
- 6:39Seals enforce transitive immutability
- 7:41System F-sub with read-only types
- 9:05Calculus soundness and benefits
- 10:28Q&A on private types and mutability
- 11:36Terminology debate
- 12:39Higher-order functions with read-only
- 13:43Equivalence lemmas and gradual typing
- 14:26Seals as chaperon contracts in Racket
related talks
18mQualifying System F-sub
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
30mPlausible sealing for gradual parametricity
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
31mRethinking the Value Restriction
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
48mA History of Subtyping