Amal Ahmed
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.
- 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. Google Scholar
Digital Library
- Amal Ahmed and Matthias Blume. Typed closure conversion preserves observational equivalence. In ICFP, 2008. Google ScholarDigital Library
- Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence (Technical appendix), 2008. Available at: http://ttic.uchicago.edu/~amal/papers/sdri/ Google ScholarDigital Library
- Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. Transactions on Programming Languages and Systems, 23(5):657--683, 2001. Google ScholarDigital Library
- Anindya Banerjee and David A. Naumann. Ownership confinement ensures representation independence in object-oriented programs. Journal of the ACM, 52(6):894--960, 2005. Google ScholarDigital Library
- Anindya Banerjee and David A. Naumann. State based ownership, reentrance, and encapsulation. In ECOOP, 2005. Google ScholarDigital Library
- Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In TLCA, 2005. Google ScholarDigital Library
- Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. Relational parametricity for references and recursive types, July 2008. Draft, submitted for publication.Google Scholar
- Nina Bohr. Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD thesis, IT University of Copenhagen, 2007.Google Scholar
- Nina Bohr and Lars Birkedal. Relational reasoning for recursive types and references. In APLAS, 2006. Google ScholarDigital Library
- Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin. 2007. Google ScholarDigital Library
- Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules. In POPL, 2003. Google ScholarDigital Library
- Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, 2006. Google ScholarDigital Library
- Vasileios Koutavas and Mitchell Wand. Reasoning about class behavior. In FOOL/WOOD, 2007.Google Scholar
- Xavier Leroy. Applicative functors and fully transparent higher-order modules. In POPL, 1995. Google ScholarDigital Library
- Paul-André Melliès and Jérôme Vouillon. Recursive polymorphic types and parametricity in an operational framework. In LICS, 2005. Google ScholarDigital Library
- John C. Mitchell. Representation independence and data abstraction. In POPL, 1986. Google ScholarDigital Library
- Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5&6):865--911, September 2008. Google ScholarDigital Library
- Benjamin C. Pierce and Davide Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM, 47(3):531--586, 2000. Google ScholarDigital Library
- Andrew Pitts. Typed operational reasoning. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, pages 245--289. The MIT Press, 2005.Google Scholar
- Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In HOOTS, 1998. Google ScholarDigital Library
- Uday Reddy and Hongseok Yang. Correctness of data representations involving heap data structures. In ESOP, 2003. Google ScholarDigital Library
- John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.Google Scholar
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002. Google ScholarDigital Library
- Claudio V. Russo. Non-dependent types for Standard ML modules. In PPDP, 1999. Google ScholarDigital Library
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. In LICS, 2007. Google ScholarDigital Library
- Eijiro Sumii and Benjamin Pierce. A bisimulation for dynamic sealing. Theoretical Computer Science, 375(1-3):161--192, 2007. Google ScholarDigital Library
- Eijiro Sumii and Benjamin Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):1--43, 2007. Google ScholarDigital Library
- Janis Voigtländer and Patricia Johann. Selective strictness and parametricity in structural operational semantics, inequationally. Theoretical Computer Science, 388(1-3):290--318, 2007. Google ScholarDigital Library
Index Terms
- State-dependent representation independence
Recommendations
State-dependent representation independence
POPL '09Mitchell'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 ...
A relational modal logic for higher-order stateful ADTs
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThe method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, ...
A relational modal logic for higher-order stateful ADTs
POPL '10The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, ...
Comments