(short) paper available
The following paper
is available by anonymous ftp from
The file is in the directory
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 
`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 firstname.lastname@example.org mailing list).