[Prev][Next][Index][Thread]
ftp papers on Constructive Logics
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