一句话：提出类型导向的统一内存模型 LoCalMem，用显式边界类型统一本地自适应序列化与内容寻址的分布式去重，并证明其可靠性与局部性。
函数式语言通过结构共享支持非破坏性更新，但内存表示面临两难：指针堆保留共享却损害布局局部性，序列化堆局部性好却造成复制。Gibbon 用自适应序列化在更新过程中逐步提升局部性、在必须共享处回退为间接引用，但缺乏形式化基础。本文形式化 Gibbon 内存模型的关键部分（静态与动态语义），并提出一个统一的类型导向内存模型，给出两种实现：面向本地执行的位置寻址内存（LAM）与面向持久化和分布式去重的内容寻址内存（CAM）。二者共同的核心抽象是显式边界数据类型，用以在共享与序列化之间进行中介：在 LAM 中边界支撑自适应序列化并助力可靠性证明，在 CAM 中同样的边界支持基于滚动哈希切割的高效分块策略，并通过相邻边界间 token 数的静态界限定重序列化开销。作者在纯函数式设定下用操作语义形式化两个模型，证明其相对于普通函数式值的可靠性；对 CAM 还证明了局部性定理：更新所需工作量与修改路径深度成正比而非与值的大小成正比。由此，大型持久化值可增量更新，未变子结构跨版本、跨机器自动共享。
Functional programming languages support non-destructive updates via structural sharing, creating a fundamental tradeoff in memory representation: pointer-based heaps preserve sharing but degrade layout locality, while serialized heaps prioritize locality at the cost of duplication. Gibbon addresses this tradeoff by using adaptive serialization: as the program updates its heap, the memory manager improves locality through serialization, falling back to indirection where sharing is unavoidable. In this work, we formalize key parts of Gibbon's memory model, including the statics and dynamics of adaptive serialization. We then present a unified, type-directed memory model with two realizations: location-addressable memory (LAM) for local execution and content-addressable memory (CAM) for persistence and distributed deduplication. The key abstraction in both models is a notion of explicit boundary datatypes mediating between sharing and serialization. In LAM, boundaries facilitate adaptive serialization and enable our soundness proofs. In CAM, the same boundaries enable an efficient chunking policy, whereby candidate chunk points are selected via rolling-hash cuts. We establish efficiency via a static bound on the number of tokens between consecutive boundaries, bounding reserialization costs. We work in the purely functional setting, where structural sharing is observationally transparent and content-addressed identity is well defined. We formalize both models with operational semantics and prove soundness with respect to ordinary functional values. For CAM, we prove a locality theorem: the work required for an update scales with the depth of the modified path rather than the size of the value. Consequently, large persistent values can be updated incrementally, with unchanged substructures shared automatically across versions and across machines. Together, these results show that a single boundary discipline can unify local structural sharing and distributed deduplication within one type-theoretic foundation.
@article{RaineyBVKKS26,
title = {LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory},
author = {Michael Rainey and Michael H. Borkowski and Michael Vollmer and Chaitanya S. Koparkar and Mikah Kainen and Vidush Singhal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828688}
}