[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