A Minimal Language for Mutable Data Structures

Abstract

This thesis presents the design of a minimal imperative language for reasoning about mutable data structures and memory effects. The language separates variable introduction, alias creation, and mutation into distinct operators and makes allocation behavior explicit in the program text. Since locations are introduced only through visible constructs, sharing and memory growth can be reasoned about from the source code. The results show how different construction patterns produce distinct memory topologies, traversal styles, update behavior and sharing relationships. The thesis also explores the limitations of a simple structural type system in combination with mutable linked structures.