State-dependent representation independence

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 traction is achieved through existential typing), as well as - or Java-like languages (where data abstraction is achieved through the use of local mutable state). However, none of these apaddresses 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 s...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Amal Ahmed, Derek Dreyer, Andreas Rossberg
• Keywords: Generative Adts, Local Mutable State, POPL 2009, Programming Languages, Representation Independence