[Prev][Next][Index][Thread]
"A NEW DECONSTRUCTIVE LOGIC: LINEAR LOGIC"
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
An extended and revised version of our paper
"A NEW DECONSTRUCTIVE LOGIC: LINEAR LOGIC"
is now available by anonymous ftp, at
ftp boole.logique.jussieu.fr in the directory pub/scratch/DJS
Via WWW: http://www.logique.jussieu.fr/www.hars/djs.html
ABSTRACT:
The main concern of this paper is the design of a noetherian and
confluent normalization for {\bf LK}$^2$ (that is, classical second
order predicate logic presented as a sequent calculus). The method we
present is powerful: since it allows us to recover as fragments
formalisms as seemingly different as Girard's {\bf LC} and Parigot's
$\lambda\mu$, {\bf FD}, delineates other viable systems as well, and
gives means to extend the Krivine/Leivant paradigm of
`programming-with-proofs' to classical logic; it is painless: since we
reduce strong normalization and confluence to the same properties for
linear logic (for non-additive proof nets, to be precise) using
appropriate embeddings (so-called decorations); it is unifying: it
organizes known solutions in a simple pattern that makes apparent the
how and why of their making. A comparison of our method to that of
embedding {\bf LK} into {\bf LJ} (intuitionistic sequent calculus)
brings to the fore the latter's defects for these `deconstructive
purposes'.
V.Danos-J.B. Joinet-H.Schellinx