| |
VOLUME 5, ISSUE 3, PAPER 7
|
Relational Parametricity for Computational Effects
|
©Rasmus Ejlers Møgelberg, IT University of Copenhagen
©Alex Simpson, LFCS, School of Informatics, University of Edinburgh
|
Abstract
According to Strachey, a polymorphic program is parametric if it applies a
uniform algorithm independently of the type instantiations at which it is
applied. The notion of relational parametricity, introduced by Reynolds, is one
possible mathematical formulation of this idea. Relational parametricity
provides a powerful tool for establishing data abstraction properties, proving
equivalences of datatypes, and establishing equalities of programs. Such
properties have been well studied in a pure functional setting. Many programs,
however, exhibit computational effects, and are not accounted for by the
standard theory of relational parametricity. In this paper, we develop a
foundational framework for extending the notion of relational parametricity to
programming languages with effects.
|
Publication date: August 9, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(3:7)2009
Hit Counts: 1848 |
 Creative Commons | |
