Cahiers du Centre de Logique, vol. 8


Ph. DE GROOTE (ed.), The Curry-Howard Isomorphism
volume 8 of the Cahiers du Centre de logique, Academia, Louvain-la-Neuve (Belgium), 1995, 364 pages
ISBN 2-87209-363-X

This Cahier can be ordered from the publisher Academia-L'Harmattan.


This volume is devoted to the Formulae-as-Types correspondence, also widely known as the 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.

Table of contents

Curry, H. B. – Feys, R.

The basic theory of functionality. Analogies with propositional algebra


Howard, W. A.

The Formulae-as-Types Notion of Construction


De Bruijn, N. G.

On the roles of types in mathematics


Gallier, J.

On the Correspondence between proofs and lambda-terms


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



7 septembre 2009