Jean-Yves G. Proofs and Types 1989

Textbook in PDF format

Sense, Denotation and Semantics.
Natural Deduction.
The Curry-Howard Isomorphism.
The Normalisation Theorem.
Sequent Calculus.
Strong Normalisation Theorem.
Goedel'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