Paper Available

I should like to announce the availability of the following paper from
my home page


		     Observations on a Linear PCF
			 (Preliminary Report)

			     G.M. Bierman

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

title="Observations on a linear {PCF}",
institution="University of Cambridge Computer Laboratory",