Proofs And Types

A book by JeanYvesGirard, available online:

• http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html

Based on a short graduate course on typed lambda-calculus. ISBN 0521371813

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

---

CategoryBook CategoryProof