LLL : the paper

• To: lineaire <linear@cs.stanford.edu>
• Subject: LLL : the paper
• From: girard@lmd.univ-mrs.fr (Jean-Yves GIRARD)
• Date: Mon, 6 Feb 95 11:52:26 +0200
• Approved: types@dcs.gla.ac.uk

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)

• Prev: MFPS Program and Registration Information
• Next: Isabelle course -- brief notice
• Index(es):
  • Main
  • Thread