State-dependent representation independence

ABSTRACT

Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity -- two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation between their type representations that is preserved by their operations. There have been a number of methods proposed for proving representation independence in various pure extensions of System F (where data abstraction is achieved through existential typing), as well as in Algol- or Java-like languages (where data abstraction is achieved through the use of local mutable state). However, none of these approaches addresses the interaction of existential type abstraction and local state. In particular, none allows one to prove representation independence results for generative ADTs -- i.e. ADTs that both maintain some local state and define abstract types whose internal representations are dependent on that local state.

In this paper, we present a syntactic, logical-relations-based method for proving representation independence of generative ADTs in a language supporting polymorphic types, existential types, general recursive types, and unrestricted ML-style mutable references. We demonstrate the effectiveness of our method by using it to prove several interesting contextual equivalences that involve a close interaction between existential typing and local state, as well as some well-known equivalences from the literature (such as Pitts and Stark's "awkward" example) that have caused trouble for previous logical-relations-based methods.

The success of our method relies on two key technical innovations. First, in order to handle generative ADTs, we develop a possible-worlds model in which relational interpretations of types are allowed to grow over time in a manner that is tightly coupled with changes to some local state. Second, we employ a step-indexed stratification of possible worlds, which facilitates a simplified account of mutable references of higher type.

REFERENCES

• 1: Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. Extended/corrected version of this paper available as Harvard University TR-01-06.
• 2: Amal Ahmed , Matthias Blume, Typed closure conversion preserves observational equivalence, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 3: Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence (Technical appendix), 2008. Available at: http://ttic.uchicago.edu/~amal/papers/sdri/
• 4: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 5: Anindya Banerjee , David A. Naumann, Ownership confinement ensures representation independence for object-oriented programs, Journal of the ACM (JACM), v.52 n.6, p.894-960, November 2005 [doi>10.1145/1101821.1101824]
• 6: Anindya Banerjee and David A. Naumann. State based ownership, reentrance, and encapsulation. In ECOOP, 2005.
• 7: Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In TLCA, 2005.
• 8: Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. Relational parametricity for references and recursive types, July 2008. Draft, submitted for publication.
• 9: Nina Bohr. Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD thesis, IT University of Copenhagen, 2007.
• 10: Nina Bohr and Lars Birkedal. Relational reasoning for recursive types and references. In APLAS, 2006.
• 11: Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin. 2007.
• 12: Derek Dreyer , Karl Crary , Robert Harper, A type system for higher-order modules, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-249, January 15-17, 2003, New Orleans, Louisiana, USA
• 13: Vasileios Koutavas , Mitchell Wand, Small bisimulations for reasoning about higher-order imperative programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.141-152, January 11-13, 2006, Charleston, South Carolina, USA
• 14: Vasileios Koutavas and Mitchell Wand. Reasoning about class behavior. In FOOL/WOOD, 2007.
• 15: Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199476]
• 16: Paul-Andre Mellies , Jerome Vouillon, Recursive Polymorphic Types and Parametricity in an Operational Framework, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.82-91, June 26-29, 2005 [doi>10.1109/LICS.2005.42]
• 17: John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
• 18: Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5&6):865--911, September 2008.
• 19: Benjamin C. Pierce , Davide Sangiorgi, Behavioral equivalence in the polymorphic pi-calculus, Journal of the ACM (JACM), v.47 n.3, p.531-584, May 2000 [doi>10.1145/337244.337261]
• 20: Andrew Pitts. Typed operational reasoning. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, pages 245--289. The MIT Press, 2005.
• 21: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 22: Uday Reddy and Hongseok Yang. Correctness of data representations involving heap data structures. In ESOP, 2003.
• 23: John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.
• 24: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 25: Claudio V. Russo, Non-dependent Types for Standard ML Modules, Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, p.80-97, September 29-October 01, 1999
• 26: Davide Sangiorgi , Naoki Kobayashi , Eijiro Sumii, Environmental Bisimulations for Higher-Order Languages, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.293-302, July 10-14, 2007 [doi>10.1109/LICS.2007.17]
• 27: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, v.375 n.1-3, p.169-192, April, 2007 [doi>10.1016/j.tcs.2006.12.032]
• 28: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Journal of the ACM (JACM), v.54 n.5, p.26-es, October 2007 [doi>10.1145/1284320.1284325]
• 29: Janis Voigtländer , Patricia Johann, Selective strictness and parametricity in structural operational semantics, inequationally, Theoretical Computer Science, v.388 n.1-3, p.290-318, December, 2007 [doi>10.1016/j.tcs.2007.09.014]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
abstract data types, existential types, local state, representation independence, step-indexed logical relations