Do Mutable Variables Have Reference Types?
summary
Offshoring fails for mutable variables: naive translation that treats OCaml refs as C pointers either forces ad hoc restrictions (refs only for base types, limited occurrences) or doubles allocations. The paper gives offshoring the systematic fix: one translation maps every ref to a heap pointer (simple but allocates twice), a second translation maps mutable bindings to real C variables and nonmutables to pointers, preserves semantics, enables mutation tracking, and is formalized and mechanized; implementation into metal camel is planned.
AI-written summary · about
chapters (6)
- 0:00Start
- 0:04Generating C
- 3:24Challenge
- 3:47Pointers and references
- 7:58C without mutable variables
- 12:06Formalities
related talks
37mMemory Safety Everywhere with Both Rust and Carbon
23mPattern-matching on mutable values: danger!
31mCo- and Contra-: Adding a Little Variance
31mRethinking the Value Restriction
29mMetaOCaml Theory and Implementation
32mBeyond the &: A Future for Native Smart Pointers in Rust
28mSemi-explicit polymorphic parameters
26mSemantic Encapsulation using Linking Types