Correctness of data representations involving heap data structures

S. Abramsky, K. Honda, G. McCusker, A fully abstract game semantics for general references, in: Lecture Notes in Computer Science, 1998, pp. 334–344. A. Banerjee, D.A. Naumann, Representation independence, confinement and access control, in: POPL, ACM, New York, 2002. B.P. Dunphy, Parametricity as a notion of uniformity in reflexive graphs, Ph.D. Thesis, University of Illinois, Department of Mathematics, 2002. D.R. Ghica, Semantics of dynamic variables in Algol-like languages, Master's Thesis, Queen's University, Kingston, Canada, March 1997. Launchbury, 1995, State in Haskell, J. Lisp. Symbolic Comput., 8, 293, 10.1007/BF01018827 P.B. Levy, Call-by-push-value, Ph.D. Thesis, Queen Mary, University of London, March 2001. P.B. Levy, Possible world semantics for general storage in call-by-value, in: CSL, 2002, pp. 232–246. A.R. Meyer, K. Sieber, Towards fully abstract semantics for local variables, in: Fifteenth Ann. ACM Symp. on Princ. of Program. Lang., ACM, New York, 1988, pp. 191–203. (Reprinted as Chapter 7 of [16]). Mitchell, 1988, Abstract types have existential types, ACM Trans. Program. Lang. Systems, 10, 470, 10.1145/44501.45065 Moggi, 1991, Notions of computations and monads, Inform. Comput., 93, 55, 10.1016/0890-5401(91)90052-4 O'Hearn, 2000, From Algol to polymorphic linear lambda-calculus, J. ACM, 47, 167, 10.1145/331605.331611 O'Hearn, 2001, Local reasoning about programs that alter data structures, vol. 2142, 1 P.W. O'Hearn, J. Reynolds, H. Yang, Separation and information hiding, in: ACM Symp. on Princ. of Program. Lang., ACM, New York, 2004, pp. 268–280. O'Hearn, 1992, Semantics of local variables, 217 O'Hearn, 1995, Parametricity and local variables, J. ACM, 42, 658, 10.1145/210346.210425 O'Hearn, 1997 F.J. Oles, A category-theoretic approach to the semantics of programming languages, Ph.D. Thesis, Syracuse University, 1982. U.S. Reddy, When parametricity implies naturality, Electronic manuscript, University of Birmingham, http://www.cs.bham.ac.uk/~udr/, July 1997. U.S. Reddy, Objects and classes in Algol-like languages, in: FOOL 5: Fifth Intern. Workshop on Foundations of Object-oriented Languages, January 1998, electronic proceedings at http://pauillac.inria.fr/~remy/fool/proceedings.html. Reddy, 2002, Objects and classes in Algol-like languages, Inform. Comput., 172, 63, 10.1006/inco.2001.2927 U.S. Reddy, H. Yang, Correctness of data representations involving heap data structures, in: Programming Languages and Systems: 12th European Symposium on Programming (2003), Lecture Notes in Computer Science, vol. 2618, Springer, Berlin, pp. 223–237. J.C. Reynolds, Towards a theory of type structure, in: Coll. sur la Programmation, Lecture Notes in Computer Science, vol. 19, Springer, Berlin, 1974, pp. 408–425. Reynolds, 1981, The essence of Algol, 345 J.C. Reynolds, Intuitionistic reasoning about shared mutable data structure, in: J. Davies, B. Roscoe, J. Woodcock (Eds.), Millenial Perspectives in Computer Science, Palgrave, Houndsmill, UK, 2000. E. Robinson, G. Rosolini, Reflexive graphs and parametric polymorphism, in: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, July 1994. I. Stark, Names and higher-order functions, Ph.D. Thesis, University of Cambridge Computer Laboratory, Tech. Rep. 363, 1995. Stark, 1996, Categorical models for local names, Lisp Symbolic Comput., 9, 77, 10.1007/BF01806033 Tennent, 1994, Correctness of data representations in Algol-like languages, 405 P. Wadler, The essence of functional programming, in: ACM Symp. on Princ. of Program. Lang., 1992, pp. 1–14. Wirth, 1966, A contribution to the development of Algol, Comm. ACM, 9, 413, 10.1145/365696.365702 H. Yang, Local reasoning for stateful programs, Ph.D. Thesis, The University of Illinois at Urbana-Champaign, Tech. Rep. UIUCDCS-R-2001-2227, 2001.