paper announcement

                  Announcement of a paper:

            Proof Nets ans Typed Lambda Calculus
                  I. Empires and Kingdoms


                G.Bellin and J.van de Wiele
         (Oxford University - Universite' de Paris VII)

This paper is the first part of a study of Proof Nets and of Natural
Deduction derivations as graphs with different forms of orientations.
Results reached so far include a representation of linear lambda terms
as oriented Chinese Characters Diagrams, arising in the study of
Vassiliev invariants in knot theory; a translation preserving
normalization of natural deduction for linear logic into oriented
proof-nets; conditions for orientability of proof-nets yielding
the inverse translation. In the present paper, extending previous
unpublished results by Girard, Danos, Gonthier, Joinet, Regnier,
we provide a system of first order proof-nets without boxes for
the full system of linear logic and we investigate the structure
of the subnets of a proof-net.
The paper ``Proof Nets ans Typed Lambda Calculus I. Empires and Kingdoms''
is available by anonymous ftp from 
in the directory
in the files 
          king.dvi.Z                   king.ps
use uncompress king.dvi.Z to obtain the dvi-file king.dvi. 
Comments: The reader can use this (rather long) paper in several ways. 
1. in the preface we discuss the motivations for the project and give 
an outline of some results; 
2. in the section on multiplicative proof nets we develop the theory of 
the subnets of a multiplicative proof net, based on Danos and Regnier's 
correctness condition;
3. in the Appendix II we give equivalent correctness conditions for the 
multiplicative fragment; 
4. in the sections on the additives and the exponentials we generalize 
Danos and Regnier's method to the whole system of linear logic;
we also discuss these results as a contribution to the ``elimination
of boxes''; 
5. we consider the computational complexity of some constructions; 
6. in the section on the problem of irrelevance (Weakening boxes)
we recall and discuss systems of Direct Logic, namely, Linear Logic 
with the rule of Mix (Mingle). 

We made a special effort to give proper credit for the results;
unfortunately, omission of relevant results and/or credits is always 
possible and will be corrected; please let us know.