[Prev][Next][Index][Thread]
PCF, Algol, and Parametric Polymorphism
We would like to announce the following summary paper
available by ftp:
Reducing Sequentiality and Block Structure to
Parametric Polymorphism
Peter W. O'Hearn Jon G. Riecke
Syracuse University AT&T Bell Laboratories
Finding good descriptions of sequentiality and block-structure are
notorious problems in semantics. A "good" mathematical model
should be definable without using the syntax of the language and
should (ideally) be FULLY ABSTRACT, i.e., such that denotational
equivalence coincides with observational equivalence. (Two pieces
of code are "observationally equivalent" if, when placed in any
program context, the two resultant programs return the same final
answers.) As is well known, the standard Scott model of PCF
contains "parallel" functions that distinguish observationally
equivalent terms; and most models of idealized Algol contain
elements that violate the stack discipline and distinguish
observationally equivalent terms.
In this paper we show how to build fully abstract translations---
i.e., syntactic translations that preserve observational
equivalence and inequivalence---from PCF and an idealized Algol to
a language we call PPCF+XML. PPCF+XML is PCF extended with a
parallel conditional and an ML-style polymorphic "let". The
parametric nature of the polymorphism in this language is
essential to the construction of the translations. We believe
that the translation theorems are suggestive of the potential
unifying force of the Strachey-Reynolds concept of parametricity.
To obtain the paper by anonymous ftp, proceed as follows:
ftp top.cis.syr.edu
login: anonymous
password: <your email address>
cd ohearn
binary
get ohearn-riecke.dvi
Note: The discussion in this summary paper is a little out of
date, in that it does not discuss the recent fascinating
anouncements of Abramsky-Jagadeesan-Malacaria and Hyland-Ong on
games semantics for PCF.