Programming with Explicit Effects in ReML
summary
ReML is a statically typed ML dialect that lets programmers annotate where values live and what effects occur so region-based allocation and deallocation remain stable across edits and optimizations. It integrates with MLKit’s region inference and supports region polymorphism, region-polymorphic recursion, and shallow versus deep copy discipline; adds effect constraints like no-intersecting allocations and no-modify checks; and wires into a let-spawn parallel primitive with a protection-inference pass that inserts region locks (causing allocation overhead) where threads would race. Partially implemented; formalization and some tooling remain.
AI-written summary · about
chapters (12)
- 0:00Explicit effects in ReML
- 2:55Region-based memory management
- 6:07Extending source language with regions
- 9:01Region polymorphism in functions
- 13:37Global regions and annotations
- 15:25Exomorphic and endomorphic functions
- 18:56Region substitution without outlives
- 20:43Merge sort with region recursion
- 23:11Effect constraints in ReML
- 25:19Parallelism with effects
- 27:31Future work and related work
- 28:19Q&A
related talks
28mA Formal Executable Semantics of PROMELA
22mRelaxed Memory Concurrency Re-executed
01h 11mProgramming language memory models: Problems, solutions, and directions
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
21mWeak Memory Demands Model-based Compiler Testing
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mCSL and relaxed memory
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency