[Prev][Next][Index][Thread]
Cahiers 8
The "Centre de logique" of the "Universit\'e catholique de Louvain" in
Louvain-la-Neuve (Belgium) will issue volume 8 of its "Cahiers" in
January.
This volume is edited by Philippe de Groote and is mainly devoted to
the Curry-Howard isomorphism.
===============================================================================
===============================================================================
R E F E R E N C E S
Ph. de Groote (Ed.), "The Curry-Howard isomorphism",
Volume 8 of the "Cahiers du Centre de logique" (Universit\'e catholique de
Louvain), Academia, Louvain-la-Neuve (Belgium), 1995, 364 pages.
ISBN: 2-87209-363-X, ca. BEF 1450 or US$ 50.
===============================================================================
T A B L E O F C O N T E N T S
pp. 9-13: H.B. Curry and R. Feys,
"The basic theory of functionality. Analogies with propositional algebra"
pp. 15-26: W.A. Howard,
"The Formulae-as-Types Notion of Construction"
pp. 27-54: N.G. de Bruijn,
"On the roles of types in mathematics"
pp. 55-138: J. Gallier,
"On the Correspondence between proofs and $\lambda$-terms"
pp. 139-191: H. Geuvers,
"The Calculus of Constructions and Higher Order Logic"
pp. 193-255: J.-Y. Girard,
"Linear Logic: A Survey"
pp. 257-364: J. Lipton,
"Realizability, Set Theory and Term Extraction"
===============================================================================
S U M M A R Y
This volume is devoted to
the {\it Formul\ae-as-Types correspondence}, also widely known as
the {\it Curry--Howard isomorphism}.
So far this has been studied mainly by constructive logicians.
But it has recently been revived by theoretical computer scientists, through
the program-as-proof correspondence.
The first four papers are introductory.
The volume starts with a reproduction of
the seminal papers by Curry-Feys and Howard.
Then de Bruijn motivates his Automath language, bringing to light the
program-as-proof correspondence.
Finally, the very detailed paper of Gallier presents and discusses the
correspondence between natural deduction proofs and $\lambda$-terms.
The next three papers are concerned with applications.
First, Geuvers presents the Calculus of Constructions, a typed
$\lambda$-calculus for higher order intuitionistic logic.
Next, Girard provides a survey of his linear logic.
The volume ends with a synthetic description of Intuitionistic Zermelo--%
Fraenkel set theory by Lipton, including realisability and categorical
interpretations.
Those three papers are self-contained and include extensive lists of
references.
===============================================================================
If you want more information, please write to
Marcel Crabb\'e
Universite catholique de Louvain
Departement de philosophie
crabbe@risp.ucl.ac.be
or to
Daniel Dzierzgowski
Universite catholique de Louvain
Departement de mathematique
ddz@agel.ucl.ac.be