Do Mutable Variables Have Reference Types?

TL;DR

This paper systematically investigates whether mutable variables can be modeled as reference types in imperative languages, providing general solutions without restrictions and clarifying the correspondence between references and C assignment semantics.

Contribution

It offers the first comprehensive analysis of modeling mutable variables as reference types, removing previous restrictions and clarifying the semantics of C assignment without L-values.

Findings

Identifies limitations of previous approaches to modeling mutable variables

Proposes general solutions for representing mutable variables as reference types

Clarifies the semantics of C assignment without L-values

Abstract

Implicit heterogeneous metaprogramming (a.k.a. offshoring) is an attractive approach for generating C with some correctness guarantees: generate OCaml code, where the correctness guarantees are easier to establish, and then map that code to C. The key idea is that simple imperative OCaml code looks like a non-standard notation for C. Regretfully, it is false, when it comes to mutable variables. In the past, the approach was salvaged by imposing strong ad hoc restrictions. The present paper for the first time investigates the problem systematically and discovers general solutions needing no restrictions. In the process we explicate the subtleties of modeling mutable variables by values of reference types and arrive at an intuitively and formally clear correspondence. We also explain C assignment without resorting to L-values.