2025/08/05 by Paulette Koronkevich, William J. Bowman · 1 voice
Computer Science · #Advanced Software Engineering Methodologies #Logic, programming, and type systems #Software Engineering Research
paper · doi:10.1145/3747532
openalex publication_date 2025/08/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/16
What are mutable references; what do they mean? The answers to these questions have spawned lots of important theoretical work and form the foundation of many impactful tools. However, existing semantics collapse a key distinction: which allocations does a reference depend on? In this paper, we deconstruct the space of mutable higher-order references. We formalize a novel distinction–splitting the design space of references not only into higher-order vs (full-)ground references, but also dependency of an allocation on past vs future allocations. This distinction is fundamental to a thorny issue that arises in constructing semantic models of mutable references–the type-world circularity. The issue disappears for what we call predicative references, those that only quantify over past, not future, allocations, and for non-higher-order impredicative references. We design a syntax and semantics for each point in our newly described space. The syntax relies on a type universe hierarchy, à la dependent type theory, to kind the types of allocated terms, and stratify allocations. Each type universe corresponds to a semantic Kripke world, giving a lightweight syntactic mechanism to design and restrict heap shapes. The semantics bear a resemblance to work on regions, and suggest some connection between universe systems and regions, which we describe in some detail.