[Prev][Next][Index][Thread]
LLL : the paper
The following paper is available through anonymous ftp
lmd.univ-mrs.fr,dir pub/girard :
LIGHT LINEAR LOGIC
in the compressed files
LLL.dvi.Z or LLL.ps.Z
It basically contains the detailed proofs that LLL normalizes in
polytime, and that polytime functions can be represented in LLL. ELL
and light set-theory/light arithmetic are only sketched. The main
reference of this paper
PROOF-NETS : THE PARALLEL SYNTAX FOR PROOF-THEORY
is also available at the same source
Proofnets.dvi.Z or Proofnets.ps.Z
where the proofnet technology is expounded (the paper has been
slightly updated since my previous message).
Finally a general survey paper
LINEAR LOGIC : ITS SYNTAX AND SEMANTICS
can be obtained at the same source
Synsem.dvi.Z or Synsem.ps.Z
---
Jean-Yves GIRARD
Directeur de Recherche
CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9
<girard@lmd.univ-mrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)