# 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^{A}T_{E}X, 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:
- 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

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.