[Prev][Next][Index][Thread]
Proofs and Types (Girard et al)
Date: Tue, 2 May 89 11:07:24 BST
****************
Proofs and Types
****************
by Jean-Yves Girard
translated and with appendices by Paul Taylor and Yves Lafont
Cambridge University Press (Cambridge Tracts in T.C.S. 7) 1989
ISBN 0 521 37181 3 xi+176pp
This time last year I advertised my translation of Girard's
"Lambda Calcul Typ\'e" on "types" inviting offers to proof-read.
I would like to thank those who responded with comments, in
particular Luke Ong, Christine Paulin-Mohring, Ramon Pino,
Mark Ryan, Thomas Streicher and Bill White for their suggestions
and detailed corrections.
The original introduction, and the proof of represenatbility of
provably total functions, have been expanded, and two appendices
have been added. The book was produced in LaTeX.
At the British Colloquium on T.C.S. recently, thirty of the eighty
participants bought copies; it has also already sold out at UPenn
bookstore. So get in there quick before it's out of print!
1. Sense, Denotation and Semantics 1
2. Natural Deduction 8
3. The Curry-Howard Isomorphism 14
4. The Normalisation Theorem 22
5. Sequent Calculus 28
6. Strong Normalisation Theorem 42
(Tait's proof using reducibility aka logical relations)
7. G\"odel's System T 47
(with Bool and Int types added)
8. Coherence Spaces 54
(stable functions, trace, Berry order)
9. Denotational Semantics of T 67
(interpretation of lambda calculus and System T using
coherence spaces; lazy natural numbers; infinity & fixed pt)
10. Sums in Natural Deduction 73
(disjunction & existential rules in ND; commuting conversions;
sum types)
11. System F 82
(rules; many simple examples of inductive data types)
12. Coherence Semantics of the Sum 95
(difficulty of interpreting sum types in coherence spaces
leads to linear connectives & linear functions; dI-domains)
13. Cut Elimination (Hauptsatz) 105
(proof of cut elimination for sequent calculus; application
to PROLOG)
14. Strong Normalisation for F 114
15. Representation Theorem 120
(proof that functions are representable in F iff they are
provably total in second order (Heyting) arithmetic; the
argument essentially uses realisability, but this is not
introduced formally).
A. Semantics of System F (by Paul Taylor) 132
(detailed construction of universal types in coherence
spaces, with explicit calculations of simple cases and
sketch for natural numbers)
B. What is Linear Logic (by Yves Lafont) 150
(linear sequent calculus; proof nets; turbo-cut elimination)
Bibliography 162
Index & index of notatation (extensive!) 166
The early parts of the book are suitable for a first course in
logic; the later parts are advanced or research material.