Girard in translation

To: types@theory.lcs.mit.edu
Subject: Girard in translation
From: Paul Taylor <mcvax!doc.ic.ac.uk!pt@uunet.UU.NET>
Date: Mon, 16 May 88 11:31:30 BST

                     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
within a few weeks, please email me your postal address.