Proofs and Types

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 \lambda-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.

References

• The book is available for free as a pdf file on Paul Taylor's website.

@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}
}