Proofs and Types

Jean-Yves Girard, Yves Lafont and Paul Taylor

1989

By Jean-Yves Girard, translated and with appendices by Paul Taylor 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.

As the book is now out of print, we have provided it on-line in various formats:

• PDF - for on-line viewing with xpdf or acroread.
• DVI - warning: uses the St Mary Road symbol font for the ``par'' symbol.
• compressed PostScript two-up - recommended for printing, if you have a two-sided printer with European A4 paper.
• compressed PostScript - full size.

The 600dpi on-line version, unlike the 300dpi printed one, uses Paul's proof tree macros.

List of chapter titles:

1. Sense, Denotation and Semantics
2. Natural Deduction
3. The Curry-Howard Isomorphism
4. The Normalisation Theorem
5. Sequent Calculus
6. Strong Normalisation Theorem
7. Gödel's system T
8. Coherence Spaces
9. Denotational Semantics of T
10. Sums in Natural Deduction
11. System F
12. Coherence Semantics of the Sum
13. Cut Elimination (Hauptsatz)
14. Strong Normalisation for F
15. Representation Theorem

Appendices: