[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