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

(short) paper available





The following paper
     LC-nets.dvi.Z
is available by anonymous ftp from
     theory.doc.ic.ac.uk
The file is in the directory
     /papers/Bellin
use uncompress to obtain the dvi-files.

A few comments on the content:

1. The paper LC-nets provides a solution to a question in Girard [1991]
`A new constructive logic: classical logic'. Recall that LC formalizes
classical logic and has canonical translations into LJ and also LL.

To see why this is not just a straightforward adaptation of usual
LL-proof-nets to LC, notice that a sequent
                   |- A1,...,An ; Q
has an interpretation of the form
                   ! X1 times ... times ! Xn  |-  ! X.
Thus to find a system of proof-nets for LC means to produce a method
to remove a specific class of !-boxes.

2. To do this we introduce the notion of privileged empire; the fact that
such a simple modification of the notions of kingdom and empire is enough
to do the job is another sign of the utility of (what one could call)
the `quasi-topology of subnets'. A detailed presentation of the relevant
results is in the paper by Bellin and van de Wiele `Proof-nets and
typed lambda -calculus' which will be available very soon here (as other
EEC cooperative projects, its completion takes longer than expected).

I would like to know recent results in the area of LC or LU
(I have not recently received any announcement on the topic
from the linear@cs.stanford.edu mailing list).

Gianluigi Bellin