Cahiers du Centre de Logique, vol. 8

References

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

Summary

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

October 23, 2015