Cahiers du Centre de Logique,
vol. 8
References
Ph. DE GROOTE (ed.),
The CurryHoward Isomorphism
volume 8 of the Cahiers du Centre de logique, Academia, LouvainlaNeuve
(Belgium), 1995, 364 pages
ISBN 287209363X
This Cahier can be ordered from the publisher AcademiaL'Harmattan.
Summary
This volume is devoted to the FormulaeasTypes correspondence,
also widely known as the CurryHoward isomorphism.
So far this has been studied mainly by constructive logicians.
But it has recently been revived by theoretical computer scientists,
through the programasproof correspondence.
The first four papers are introductory. The volume starts with
a reproduction of the seminal papers by CurryFeys and Howard.
Then de Bruijn motivates his Automath language, bringing to light
the programasproof correspondence. Finally, the very detailed
paper of Gallier presents and discusses the correspondence between
natural deduction proofs and lambdaterms.
The next three papers are concerned with applications. First,
Geuvers presents the Calculus of Constructions, a typed lambdacalculus
for higher order intuitionistic logic. Next, Girard provides a
survey of his linear logic. The volume ends with a synthetic description
of Intuitionistic ZermeloFraenkel set theory by Lipton, including
realisability and categorical interpretations. Those three papers
are selfcontained and include extensive lists of references.
Table of contents
Curry, H. B. – Feys, R.

The basic theory of functionality. Analogies with propositional
algebra



Howard, W. A.

The FormulaeasTypes Notion of Construction


De Bruijn, N. G.

On the roles of types in mathematics


Gallier, J.

On the Correspondence between proofs and lambdaterms


Geuvers, H.

The Calculus of Constructions and Higher Order Logic


Girard, J.Y.

Linear Logic: A Survey


Lipton, J.

Realizability, Set Theory and Term Extraction










17 l 16 l 15 l 14 l 13 l 12 l 11 l 10 l 9 l 7 l 6 l 5 l 4 l 3 l 2 l 1


