HTTP/2 200 content-type: text/html last-modified: Mon, 02 Feb 2009 16:46:01 GMT accept-ranges: bytes content-encoding: gzip vary: Accept-Encoding content-length: 2229 date: Sat, 17 Jan 2026 16:17:21 GMT server: LiteSpeed alt-svc: h3=":443"; ma=2592000, h3-29=":443"; ma=2592000, h3-Q050=":443"; ma=2592000, h3-Q046=":443"; ma=2592000, h3-Q043=":443"; ma=2592000, quic=":443"; ma=2592000; v="43,46"

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 L^AT_EX, 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:

• 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:

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.