[Prev][Next][Index][Thread]
Paper available
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is now available:
A CLASSICAL LINEAR LAMBDA CALCULUS
G.M. Bierman
University of Cambridge Computer Laboratory
Technical Report 401
July 1996
Abstract:
This paper proposes and studies a typed $\lambda$-calculus for
classical linear logic. I shall give an explanation of a
multiple-conclusion formulation for classical logic due to Parigot and
compare it to more traditional treatments by Prawitz and others. I
use Parigot's method to devise a natural deduction formulation
of classical linear logic. This formulation is compared in detail to
the sequent calculus formulation. In an appendix I shall also
demonstrate a somewhat hidden connexion with the paradigm of control
operators for functional languages which gives a new computational
interpretation of Parigot's techniques.
This paper is an extended version of the paper "Towards a classical
linear lambda calculus", which is to appear in the Proceedings of the
Tokyo Linear Logic Meeting. (ENTCS)
Both these papers can be obtained from my homepage:
http://www.cl.cam.ac.uk/users/gmb
or by anonymous ftp from theory.doc.ic.ac.uk
in directory /theory/imported/BiermanGM.
A BiBTeX entry for this paper is:
@techreport{bierman96:cll,
author="G.M.~Bierman",
title="A Classical Linear $\lambda$-calculus",
institution="University of Cambridge Computer Laboratory",
number=401,
month=jul,
year=1996
}