TypeDis: A Type System for Disentanglement
summary
TypeDis is a type system that guarantees any well-typed program is disentangled and so permits task-local, synchronization-free garbage collection; it annotates heap types with timestamps in types, lets timestamps change at joins via subtiming, and supports polymorphism over types and timestamps plus iso-recursive types. The complex par primitive retimestamps child allocations to the parent, the system is sound via a logical relation mechanized in Rocq using DisLog2 mechanization, and artifacts and case studies (parallel for, duplication with concurrent hashing) are available and evaluated.
AI-written summary · about
chapters (16)
- 0:00TypeDis introduction
- 1:13Disentanglement in parallel programs
- 3:03Disentanglement enables memory management
- 4:07Separation logic to type system
- 5:33Type system core with timestamps
- 7:22Functions and timestamp annotations
- 9:14Type of parallel primitive par
- 11:41Type polymorphism added
- 13:06Typing judgment and invariants
- 14:30Logical graphs and subtiming
- 16:19Final type of par with constraints
- 17:23Subtiming rules for data
- 18:04Recursive parallel loops support
- 18:47Soundness proof in Iris
- 19:51Features and case studies
- 20:33Q&A
related talks
40mDomain Specific Type Systems
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
21mPolymorphic Type Inference for Dynamic Languages
34mGraded Monads and Type-Level Programming for Dependence Analysis
28mType-directed Program Transformation for Constant-Time Enforcement
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
42mDOT: Scala Types from Theory to Practice
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...