[Prev][Next][Index][Thread]

paper available by anonymous ftp

Date: Mon, 20 Jul 92 12:13:05 -0400

Yielding to the pressure of modern technology, I have decided
to make the following paper available by anonymous ftp:

       On Girard's "Candidats de r\'eductibilit\'e".


Although this paper has already been  published in a volume 
"Logic and Computer Science" edited by P. Odifreddi (Academic Press),
I still get a fair amount of requests, and anonymous ftp
seems like the ideal solution.

(Note: a few mistakes in the book version have been corrected)

Abstract: We attempt to elucidate the conditions required
on Girard's candidates of reducibility (in French, ``candidats de
reductibilit\'e'') in order to establish certain properties of
various typed lambda calculi, such as strong normalization
and Church-Rosser property. We present two generalizations of 
the candidates of reducibility, an untyped version in the line of
Tait and Mitchell, and
a typed version which is an adaptation of Girard's original method.
As an application of this general result, we give two proofs of
strong normalization for the second-order polymorphic lambda
calculus under $\beta\eta$-reduction (and thus under  $\beta$-reduction). 
We present two sets of conditions for the typed version of the candidates. 
The first set consists of conditions similar to those used by Stenlund 
(basically the typed version of Tait's conditions), 
and the second set consists of Girard's original conditions. 
We also compare these conditions, and prove that
Girard's conditions are stronger than Tait's conditions.
We give a new proof of the Church-Rosser theorem
for both $\beta$-reduction and $\beta\eta$-reduction, 
using the modified version of Girard's method.
We also compare various proofs that have appeared in the literature.
We conclude by sketching the extension of the above results to
Girard's higher-order polymorphic calculus $\F_{\omega}$ 
and in appendix 1, to $\F_{\omega}$  with product types.


This paper has been segmented into four files:

sngirard1.dvi.Z
sngirard2.dvi.Z
sngirard3.dvi.Z
sngirard4.dvi.Z

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

Then, use the unix "uncompress" command on this file to
get the dvi file(s).

-- Jean