[Prev][Next][Index][Thread]

paper announcement



                  Announcement of a paper:

            Proof Nets ans Typed Lambda Calculus
 
                  I. Empires and Kingdoms

                            by 

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

Abstract: 
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 
                    theory.doc.ic.ac.uk
in the directory
                    /papers/Bellin
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.