# Paper Available


I should like to announce the availability of the following paper from

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
}