[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