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

Paper available by ftp




I just completed the following paper to appear in the
"Cahiers du Centre de Logique" of the Universite' Catholique
de Louvain.

``On the Correspondence Between Proofs and lambda-Terms''

Abstract. The correspondence between natural deduction proofs
and \lambda-terms is presented and discussed.  A variant of the
reducibility method is presented, and a general theorem for
establishing properties of typed (first-order) \lambda-terms is
proved.  As a corollary, we obtain a simple proof of the Church-Rosser
property, and of the strong normalization property, for the typed
\lambda-calculus associated with the system of (intuitionistic)
first-order natural deduction, including all the connectors
\rightarrow, \times, +, \forall, \exists, and \false
(falsity) (with or without \eta-like rules).

-- Jean

-------------------------------------------------------------
The above paper can be retrieved by anonymous ftp using the
instructions below. The file name is:

cahiers2.dvi.Z

% 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