NDLI: State-dependent representation independence

Content Provider	ACM Digital Library
Author	Rossberg, Andreas Ahmed, Amal Dreyer, Derek
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.
Starting Page	340
Ending Page	353
Page Count	14
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1594834.1480925
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	44
Issue Number	1
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Local state Representation independence Abstract data types Existential types Step-indexed logical relations
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

State-dependent representation independence

A relational modal logic for higher-order stateful ADTs

Non-parametric parametricity

Programming with binders and indexed data-types

Fully-abstract compilation by approximate back-translation

Indexed codata types

The marriage of bisimulations and Kripke logical relations

Inductive reasoning about effectful data types

A bisimulation for type abstraction and recursion

State-dependent representation independence

Similar Documents

State-dependent representation independence

A relational modal logic for higher-order stateful ADTs

Non-parametric parametricity

Programming with binders and indexed data-types

Fully-abstract compilation by approximate back-translation

Indexed codata types

The marriage of bisimulations and Kripke logical relations

Inductive reasoning about effectful data types

A bisimulation for type abstraction and recursion

State-dependent representation independence