LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Published in ICFP 2026, 2026
Pointer-based heaps preserve sharing but degrade locality, while serialized heaps prioritize locality at the cost of duplication. LoCalMem formalizes the statics and dynamics of Gibbon’s adaptive serialization, presenting location-addressable and content-addressable memory models with a shared typed-data foundation, accompanied by mechanized soundness proofs in Rocq and locality proofs in Lean.
Recommended citation: Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, Vidush Singhal. (2026). "LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory." Proceedings of the ACM on Programming Languages, 10(ICFP), 461–493.
Download Paper