[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.