Abstract
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 is found that the correspondences between data representations are not simply relations between states, but more intricate correspondences that also need to keep track of visible locations whose pointers can be stored and leaked.
Chapter PDF
References
Abramsky, S., Honda, K., and McCusker, G. A fully abstract game semantics for general references. In LICS 1998 (1998), pp. 334–344.
Banerjee, A., and Naumann, D. A. Representation independence, confinement and access control. In POPL 2002 (2002), ACM.
Dunphy, B. P. Parametricity as a Notion of Uniformity in Reflexive Graphs. PhD thesis, University of Illinois, Dep. of Mathematics, 2002.
Ghica, D. R. Semantics of dynamic variables in Algol-like languages. Master’s thesis, Queen’s University, Kingston, Canada, Mar 1997. (available electronically from ).
Ghica, D. R. Parameters and linked structures in algol-like languages. In Report of the Dagstuhl Seminar 98261: The Semantic Challenge of Object-oriented Programming (1998), Schloss Dagstuhl.
Launchbury, J., and Peyton Jones, S. L. State in Haskell. J. Lisp and Symbolic Comput. 8, 4 (1995), 293–341.
Levy, P. B. Call-by-Push-Value. PhD thesis, Queen Mary, University of London, March 2001.
Levy, P. B. Possible world semantics for general storage in call-by-value. In CSL 2002 (2002), pp. 232–246.
Meyer, A. R., and Sieber, K. Towards fully abstract semantics for local variables. In Fifteenth Ann. ACM Symp. on Princ. of Program. Lang. (1988), ACM, pp. 191–203. (Reprinted as Chapter 7 of [15]).
Mitchell, J. C., and Plotkin, G. D. Abstract types have existential types. ACM Trans. Program. Lang. Syst. 10, 3 (1988), 470–502.
O’Hearn, P., Reynolds, J., and Yang, H. Local reasoning about programs that alter data structures. In CSL 2001 (Berlin, 2001), L. Fribourg, Ed., vol. 2142 of LNCS, Springer-Verlag, pp. 1–19.
O’Hearn, P. W., and Reynolds, J. C. From Algol to polymorphic linear lambda-calculus. J. ACM 47, 1 (2000), 167–223.
O’Hearn, P. W., and Tennent, R. D. Semantics of local variables. In Applications of Categories in Computer Science, M. P. Fourman, P. T. Johnstone, and A. M. Pitts, Eds. Cambridge Univ. Press, 1992, pp. 217–238.
O’Hearn, P. W., and Tennent, R. D. Parametricity and local variables. J. ACM 42, 3 (1995), 658–709. (Reprinted as Chapter 16 of [15]).
O’Hearn, P. W., and Tennent, R. D. Algol-like Languages (Two volumes). Birkhäuser, Boston, 1997.
Oles, F. J. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, 1982.
Reddy, U. S. When parametricity implies naturality. Electronic manuscript, July 1997. URL http://www.cs.bham.ac.uk/~udr.
Reddy, U. S. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on Foundations of Object-oriented Languages (Jan 1998), electronic proceedings at http://pauillac.inria.fr/~remy/fool/proceedings.html.
Reddy, U. S. Objects and classes in Algol-like languages. Information and Computation 172 (2002), 63–97.
Reynolds, J. C. Towards a theory of type structure. In Coll. sur la Programmation, vol. 19 of LNCS. Springer-Verlag, 1974, pp. 408–425.
Reynolds, J. C. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, Eds. North-Holland, 1981, pp. 345–372. (Reprinted as Chapter 3 of [15]).
Reynolds, J. C. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science. Palgrave, 2000.
Robinson, E., and Rosolini, G. Reflexive graphs and parametric polymorphism. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science (July 1994), IEEE Computer Society Press.
Stark, I. Names and higher-order functions. Technical Report 363, University of Cambridge Computer Laboratory, April 1995.
Stark, I. Categorical models for local names. Lisp and Symbolic Computation 9, 1 (Feb. 1996), 77–107.
Tennent, R. D. Correctness of data representations in Algol-like languages. In A Classical Mind: Essays in Honor of C. A. R. Hoare, A. W. Roscoe, Ed. Prentice-Hall International, 1994, pp. 405–417.
Wirth, N., and Hoare, C. A. R. A contribution to the development of Algol. Comm. ACM 9, 6 (June 1966), 413–432.
Yang, H. Local reasoning for stateful programs. Tech. Rep. UIUCDCS-R-2001-2227, University of Illinois, Dep. of Computer Science, July 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reddy, U.S., Yang, H. (2003). Correctness of Data Representations Involving Heap Data Structures. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_16
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive