[Prev][Next][Index][Thread]
Paper Available
I should like to announce the availability of the following paper from
my home page
http://www.cl.cam.ac.uk/users/gmb
Observations on a Linear PCF
(Preliminary Report)
by
G.M. Bierman
Abstract:
This paper considers some theoretical and practical issues concerning
the use of linear logic as a logical foundation of functional
programming languages such as Haskell and SML. First I give an
operational theory for a linear PCF: the (typed) linear
$\lambda$-calculus extended with booleans, conditional and
non-termination. An operational semantics is given which corresponds
in a precise way to the process of $\beta$-reduction which originates
from proof theory. Using this operational semantics I define notions
of observational equivalence (sometimes called contextual
equivalence). Surprisingly, the linearity of the language forces a
reworking of the traditional notion of a context (the details are
given in an appendix). A co-inductively defined notion, applicative
bisimularity, is developed and compared with observational
equivalence using a variant of Howe's method. Interestingly the
equivalence of these two notions is greatly complicated by the
linearity of the language. These equivalences are used to study a
call-by-name translation of PCF into linear PCF. It is shown that this
translation is adequate but not fully abstract. Finally I show how
Landin's SECD machine can be adapted to execute linear PCF programs.
A BiBTeX entry for this paper is
@techreport{bierman97,
author="G.M.~Bierman",
title="Observations on a linear {PCF}",
institution="University of Cambridge Computer Laboratory",
number=412,
month=jan,
year=1997
}