Correctness of data representations involving heap data structures

While the semantics of local variables in programming languages is by now well-understood, the semantics of pointer-addressed heap variables is still an outstanding issue. In particular, the commonly assumed relational reasoning principles for data representations have not been validated in a semantic model of heap variables. In this paper, we define a parametricity semantics for a Pascal-like language with pointers and heap variables which gives such reasoning principles. It turns out that the correspondences between data representations cannot simply be relations between states, but more intricate correspondences that also need to keep track of visible locations whose pointers can be stored and leaked.