Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
summary
The paper shows that by restricting the typing rule for references (rather than dropping distributivity or adding a global value restriction) bidirectional typing restores type soundness for distributive intersection subtyping with mutable references; it retains an unrestricted intersection-introduction rule and distributivity. The authors implement CP with references, model a modular live‑variable analysis, and mechanize proofs with Coq formalization; artifacts are available and functionally evaluated, so the approach both compiles and reproduces.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:22Imperative computational programming
- 1:48Expression problem with modular traits
- 3:37Intersection types in ICP
- 4:21Intersection types and subtyping
- 6:08References and type system
- 7:13Type soundness with references
- 9:47Bidirectional typing
- 11:58Bidirectional typing rules
- 13:25Advantages over Davis and Fanning’s solution
- 14:30Distributivity in ICP
- 15:15Formalization and proofs
- 15:37Conclusion and Q&A
related talks
30mOn Distributive Subtyping with Finitary and Infinitary Unions and Intersections
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
15mResolution as Intersection Subtyping via Modus Ponens
15mLiberating Merges via Apartness and Guarded Subtyping
48mA History of Subtyping
19mBidirectional Higher-Rank Polymorphism with Intersection and Union Types
56mOn Type-Based Techniques for Program Manipulation
21mPolymorphic Type Inference for Dynamic Languages