# 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
}