Steps towards a theory and calculus of aliasing

TL;DR

This paper develops a new theoretical framework, graphical notation, and calculus to determine if two expressions can reference the same object at runtime, aiming to address the frame problem in programming language semantics.

Contribution

It introduces a novel theory and calculus for alias analysis, providing a foundation that could replace or complement existing methods like separation logic and shape analysis.

Findings

Provides a formal graphical notation for aliasing

Develops a mathematical calculus for alias analysis

Lays groundwork for implementation of alias detection tools

Abstract

A theory, graphical notation, mathematical calculus and implementation for finding whether two given expressions can, at execution time, denote references attached to the same object. Intended as the basis for a comprehensive solution to the "frame problem" and as a complement to, or even a replacement for, separation logic, shape analysis, ownership types and dynamic frames.