Proofs and Types is a seminal book on proof theory and type theory by logician Jean-Yves Girard.
The book originated as a set of graduate lecture notes on typed -calculus given at the Université Paris VII in the autumn term of 1986-7.
It was translated to English by Paul Taylor, and typeset by Yves Lafont. Paul Taylor and Yves Lafont also added an introduction to the semantics of System F and an introduction to Linear Logic respectively.
Girard, Jean-Yves, Yves Lafont, and Paul Taylor. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press.
@book{girard_1989,
series = {Cambridge {Tracts} in {Theoretical} {Computer} {Science}},
title = {Proofs and {Types}},
number = {7},
publisher = {Cambridge University Press},
author = {Girard, Jean-Yves and Lafont, Yves and Taylor, Paul},
year = {1989}
}