Generic Abstract Immutability Types

Aosen Xiong and Werner Dietl. Accepted at IWACO 2026, the International Workshop on Aliasing, Capabilities, and Ownership, co-located with SPLASH 2026.

Paper (PDF) Implementation

Abstract

Generic data structures are representation boundaries: an immutable list may protect its own representation while still carrying mutable payload objects, or it may treat those payloads as part of its protected state. Existing immutability systems support pieces of this story, but the interaction with generics and viewpoint adaptation is subtle. The difficulty is to distinguish protected representation from independently mutable payload while preserving soundness under generic substitution and viewpoint adaptation.

This paper presents GAIT (Generic Abstract Immutability Types), an extension of an abstract immutability type system with parametric polymorphism. GAIT uses type-parameter mutability bounds to distinguish representation from payload, and organizes its guarantees into four preservation properties: abstract-state preservation (AS), concrete-state preservation (CS), readonly-state preservation (RS), and transitive-state preservation (TS). We are mechanizing the design in Lean 4 and have implemented a prototype type checker in the EISOP Checker Framework. We evaluate the checker on approximately 26,000 non-comment lines of Java code, including the Java Collections Framework.

BibTeX

@inproceedings{Xiong2026GAIT,
  author    = {Aosen Xiong and Werner Dietl},
  title     = {Generic Abstract Immutability Types},
  booktitle = {International Workshop on Aliasing, Capabilities, and
               Ownership (IWACO)},
  year      = {2026},
  note      = {Co-located with SPLASH 2026},
}