From: jean@saul.cis.upenn.edu
Newsgroups: fj.mail-lists.types
Subject: ftp papers on Constructive Logics
Date: 27 Jul 92 17:52:08 GMT
Distribution: fj

Date: Mon, 27 Jul 92 09:52:20 -0400

Sorry, but I have been experiencing the recently discovered
joy of "anon ftp"! To make good wine, old methods should be used,
but the best way to make papers available quickly is obviously
anon ftp! (For Francophiles: anon, mais oui!)
The following papers are now available by anon ftp
(see ftp instructions at the end of this message):

       Constructive Logics. Part I: A Tutorial
       on Proof Systems and Typed $\lambda$-Calculi

       Constructive Logics. Part II:
       Linear Logic and Proof Nets


The first paper is a substantially revised, expanded, and corrected
version, of  Digital PRL Tech. Report No 8 (1991). 
I wish to acknowledge Peter Baumann's invaluable assistance 
in revising and correcting this paper.
Among the additions worth mentioning, I added a section on
invertible rules and on contraction-free (decidable) systems
for propositional intuitionistic logic (systems studied by
Vorobev in the fifties, and more recently by Dyckhoff, Hudelmaier,
and Lincoln, Scedrov, and Shankar). Also, some of the lemmas
(3 and 4) used in proving that contraction-free systems exist for classical
logic have been corrected.

The ftp file name is: conslog1.dvi.Z

This paper will be published in TCS (in 1993).

                         --------------------

The second paper is a corrected version of
Digital PRL Tech. Report No 9 (1991) (notably, lemma 30 and
theorem 4), but very few changes have been made.

The ftp file name is: conslog2.dvi.Z

Vincent Danos and myself are working on a major expansion of this
paper including material on the geometry of interaction and
dynamic algebras, unified systems of logic ({\it LU\/}),
and more good stuff!

                      -----------------------

Abstract for Part 1: The purpose of this paper is to give an exposition 
of material dealing with constructive logic, typed $\lambda$-calculi, 
and linear logic. The emergence in the past ten years of a coherent 
field of research often named ``logic and computation'' has had two major
(and related) effects: firstly, it has rocked vigorously
the world of mathematical logic; secondly, it has created a new computer
science discipline, which spans from what is traditionally called
theory of computation, to programming language design.
Remarkably, this new  body of work relies heavily on some
``old'' concepts found in mathematical logic, like
natural deduction, sequent calculus, and $\lambda$-calculus (but often
viewed in a different light), and also on some newer concepts.
Thus, it may be quite a challenge to become initiated to this new body
of work (but the situation is improving, there are now some excellent texts
on this subject matter). This paper attempts to provide a coherent
and hopefully ``gentle'' initiation to this new body of work.
We have attempted to cover the basic material on
natural deduction, sequent calculus, and typed $\lambda$-calculus, but
also to provide an introduction to Girard's linear logic, one of the most
exciting developments in logic these past six years. The first part
of these notes  gives an exposition of  background material
(with some exceptions, such as ``contraction-free'' systems
for intuitionistic propositional logic and
the Girard-translation of classical logic into
intuitionistic logic, which is new). 
The second part is devoted to more current topics such as linear logic,
proof nets, the geometry of interaction, and 
unified systems of logic ({\it LU\/}).


Abstract for Part 2: The purpose of this paper is to give an exposition 
of material dealing with constructive logics, typed $\lambda$-calculi, 
and linear logic. The first part of this paper gives an exposition of  
background material (with a few exceptions).
This second part is devoted to linear logic
and proof nets. Particular attention is given to the algebraic semantics
(in Girard's terminology, phase semantics) of linear logic.
We show how phase spaces arise as an instance of a
Galois connection. We also give a direct proof of the
correctness of the Danos-Regnier criterion for proof nets. This proof
is based on a purely graph-theoretic decomposition lemma.
As a corollary, we give an $O(n^2)$-time algorithm for
testing whether a proof net is correct. 
Although the existence of such an algorithm
has been announced by Girard, our algorithm appears to be original. 

                        -----------------------

Other papers available by anon ftp:

        THEOREM PROVING USING EQUATIONAL MATINGS
               AND RIGID $E$-UNIFICATION

           Jean Gallier, Paliath Narendran,   
             Stan Raatz, and Wayne Snyder

Paper segmented into 3 ftp files:
mate1.dvi.Z
mate2.dvi.Z
mate3.dvi.Z

This paper has appeared in J.ACM, Vol. 39, No. 2, April 1992, 
pp. 377-429.

                      --------------------

            WHAT'S SO SPECIAL ABOUT KRUSKAL'S THEOREM
                  AND THE ORDINAL $\Gamma_{0}$?
            A SURVEY OF SOME RESULTS IN PROOF THEORY

Paper segmented into 3 ftp files:
kruskal1.dvi.Z
kruskal2.dvi.Z
kruskal3.dvi.Z

This paper has appeared in APAL, Vol. 53, 1991, pp. 199-260

                      --------------------

The above paper(s) can be retrieved by anonymous ftp using the
instructions below.

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/gallier
ftp> binary
ftp> get  filename.dvi.Z
ftp> quit


-- Jean