Proofs and Types
Jean-Yves Girard, Yves Lafont and Paul Taylor
By Jean-Yves Girard,
translated and with appendices by
and Yves Lafont.
Based on a short graduate course on typed lambda-calculus given at
the Université Paris VII in the autumn term of 1986-7.
Published by Cambridge University Press
(Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0 521 37181 3;
first published 1989, reprinted with corrections 1990.
By the way, Paul translated it and Yves did the LATEX, not vice versa!
Yves also chose the notation, making it consistent through the book.
Here is the story of how the translation came about: Jean-Yves had
mentioned the notes to Paul at a conference, who obtained them and
took them to read on the train on a visit to his parents. But then he
went down with 'flu. As this was his only reading material and his
French wasn't very good, he started writing out a translation.
He later showed this to Yves, who was then his office-mate. It became
a book because of the enthusiasm of Yves and of Samson Abramsky.
As the book is now out of print, we have provided it on-line in
The 600dpi on-line version, unlike the 300dpi printed one, uses
Paul's proof tree macros.
List of chapter titles:
- Sense, Denotation and Semantics
- Natural Deduction
- The Curry-Howard Isomorphism
- The Normalisation Theorem
- Sequent Calculus
- Strong Normalisation Theorem
- Gödel's system T
- Coherence Spaces
- Denotational Semantics of T
- Sums in Natural Deduction
- System F
- Coherence Semantics of the Sum
- Cut Elimination (Hauptsatz)
- Strong Normalisation for F
- Representation Theorem
A. Semantics of System F - by Paul Taylor
B. What is Linear Logic? - by Yves Lafont
and it was derived from Girard/webpage.tex
which was last modified on 3 June 2007.