Correctness of data representations involving heap data structures

Uday Reddy, H Yang

Research output: Contribution to journalArticlepeer-review

26 Citations (Scopus)
213 Downloads (Pure)


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 or 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. (C) 2004 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)129-160
Number of pages32
JournalScience of Computer Programming
Issue number1-3
Publication statusPublished - 1 Jan 2004

ASJC Scopus subject areas

  • General Computer Science
  • Computational Theory and Mathematics


Dive into the research topics of 'Correctness of data representations involving heap data structures'. Together they form a unique fingerprint.

Cite this