Ph. de Groote (Ed.), Volume 8 of the Cahiers du Centre de logique
(Univ. catholique de Louvain), Academia, Louvain-la-Neuve (Belgium),
1995, 364 pages. ISBN: 2-87209-363-X, ca. BEF 1450 or US$ 50.
Table of Contents
Summary
Study of the Formulae-as-Types correspondence, also known as the Curry-Howard isomorphism, has been recently 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 either of
Marcel Crabbe' (crabbe@risp.ucl.ac.be) Departement de philosophie
Daniel Dzierzgowski (ddz@agel.ucl.ac.be) Departement de mathematique
both at Universite' catholique de Louvain.