[L8] ================================================ AMAST Links 02 01

                     The Curry-Howard isomorphism

   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*
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.
  *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.