Wow! eBook
CURRY HOWARD ISOMORPHISM
Author(s): CAHIERS DU CENTRE LO (Author)
- Publisher: ACADEMIA
- Publication Date: 30 Oct. 1998
- Language: French
- Print length: 364 pages
- ISBN-10: 287209363X
- ISBN-13: 9782872093632
Book Description
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 ?-terms. The next three papers are concerned with applications. First, Geuvers presents the Calculus of Constructions, a typed ?-calculus for higher-order intuitionistic logic. Next, Girard provides 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.
