Proofs and Types

Jean-Yves Girard, Yves Lafont and Paul Taylor

1987-90

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.
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 various formats: 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:

    A. Semantics of System F - by Paul Taylor
    B. What is Linear Logic? - by Yves Lafont

This is www.PaulTaylor.EU/stable/Proofs+Types.html and it was derived from Girard/webpage.tex which was last modified on 3 June 2007.