# Girard in translation

```
Typed Lambda Calculus
by Jean-Yves Girard

Yves Lafont (INRIA, formerly Imperial College) and I have translated
some graduate lecture notes (Lambda Calcul Typ\'e) and intend them to
be published in the Cambridge University Press Tracts in Theoretical
Computer Science.  The list of chapter headings is as follows:

1. Sense, Denotation and Semantics
2. Natural Deduction
3. The Curry-Howard Isomorphism
4. The Normalisation Theorem
(weak normalisation; Church-Rosser is stated without proof)
5. Sequent Calculus
6. Strong Normalisation Theorem
(introducing the notion of "reducibility" which will
be used in chapter 14)
7. Godel's System T
(with booleans and numbers; normalisation; representability)
8. Coherence Spaces
(semantics with stable maps; the domains are atomic and have
binary completeness; parallel or; trace)
9. Denotational Semantics of T
(description of interpretation of application & abstraction
using trace & function space; interpretation of booleans
and numbers with ad hoc choice of domains; fixed point)
10. Sums in Natural Deduction
(bad behaviour of rules; commutative contractions)
11. System F
(description of calculus; representation of a wide variety of
types)
12. Coherent Semantics of the Sum
(amalgamated sum doesnt satisfy rules; lifted sum; linearity;
of course; linearised sum)
13. Cut Elimination (Hauptsatz)
(proof; application to PROLOG)
14. Strong Normalisation for F
(reducibility candidates; proof)
15. Representation Theorem for F
(proof that any representable function is provably total in
second order arithmetic; converse stated without proof)

Appendix (by Paul Taylor, based on the final chapter of the notes)
Semantics of System F
(interpretation of system F with coherence spaces; explicit
notation for tokens of Pi types; proof of uniformity property)

There may be one or two other appendices.

-------------------------------

I have about a dozen copies available for circulation
to anyone WHO WOULD LIKE TO MAKE SUBSTANTIAL COMMENTS/CORRECTIONS.
These are not copies for your bookshelf (you can buy them from CUP).
I do not intend to make any further copies.

If you would like a copy, and are willing to return it annotated