[Prev][Next][Index][Thread]
Paper announcement
The following paper is obtainable by anonymous ftp from
boole.logique.jussieu.fr
It can be found in the directory pub/scratch/DJS, under the name
decostringopolaro.ps.Z
(download, uncompress, print)
The directory DJS contains several related papers (read the
README file).
---------------------------------------------------
| V. Danos, J.-B. Joinet & H. Schellinx |
| |
| "A NEW DECONSTRUCTIVE LOGIC: LINEAR LOGIC" |
---------------------------------------------------
Abstract:
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,
anyway).
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
`therapies'.