Paper announcement

  The following paper is obtainable by anonymous ftp from 


  It can be found in the directory pub/scratch/DJS, under the name


  (download, uncompress, print)

  The directory DJS contains several related papers (read the
  README file).

    |      V. Danos, J.-B. Joinet & H. Schellinx        |
    |                                                   | 

    There has been much ado about constructivizing classical connectives
    and quantifiers during the last four, five years.
    Our approach to the problem is to understand this first of all as the
    quest for a classical second order calculus equipped with a strong
    (and, as much as possible, confluent) normalization, and a 
    denotational semantics.

    Considering that there are many, seemingly unrelated, solutions, we 
    would rather classify these, than throw one more solution on the heap 
    (new solutions are going to show up as a result of the classification, 

    As the title suggests, to design such a classification we use linear
    logic, to be specific three different ways to embed Gentzen's LK into LL:
    pletho, stringo and polaro. Each one of these `therapies' gives rise to 
    a sound computational interpretation of classical logic obtained by
    `pulling back' the normalization of LL as well as its denotational 
    semantics in coherent spaces. As a by-product we recover Parigot's 
    'free deduction' (FD) and `lambda-mu', as well as Girard's LC as
    particular cases of, respectively, the pletho, stringo and polaro