Proofs and Types

Description

This book is derived from notes prepared by J-Y.Girard for a course at the University of Paris VII. It deals with the mathematical background of the application to computer science of aspects of logic. It sheds light on traditional logic material and its prospective application to computer science. Sense and denotation in logic......Page 9 The syntactic tradition......Page 11 Tarski......Page 12 Heyting......Page 13 Natural Deduction......Page 16 The calculus......Page 17 Computational significance......Page 18 Interpretation of the rules......Page 19 Identification of deductions......Page 21 The Curry-Howard Isomorphism......Page 22 Terms......Page 23 Denotational significance......Page 24 Operational significance......Page 25 Conversion......Page 26 Description of the isomorphism......Page 27 Relevance of the isomorphism......Page 28 The Church-Rosser property......Page 30 Proof of the weak normalisation theorem......Page 32 Degree and conversion......Page 33 The strong normalisation theorem......Page 34 Sequent Calculus......Page 36 Structural rules......Page 37 The ``identity'' group......Page 38 Logical rules......Page 39 Some properties of the system without cut......Page 40 Subformula property......Page 41 Asymmetrical interpretation......Page 42 Sequent Calculus and Natural Deduction......Page 43 Properties of the translation......Page 46 Reducibility......Page 49 Atomic types......Page 50 Arrow type......Page 51 Abstraction......Page 52 The theorem......Page 53 Gödel's system T......Page 54 Conversions......Page 55 Normalisation theorem......Page 56 Integers......Page 57 Representable functions......Page 59 General ideas......Page 61 The web of a coherence space......Page 63 Interpretation......Page 64 Stable functions......Page 65 Parallel Or......Page 67 Direct product of two coherence spaces......Page 68 The trace of a stable function......Page 69 Representation of the function space......Page 71 The Berry order......Page 72 Partial functions......Page 73 Types......Page 74 Terms......Page 75 Properties of the interpretation......Page 76 Integers......Page 77 Infinity and fixed point......Page 79 Defects of the system......Page 80 Standard conversions......Page 81 The need for extra conversions......Page 82 Subformula Property......Page 83 Commuting conversions......Page 84 Properties of conversion......Page 86 Empty type......Page 87 Additional conversions......Page 88 The calculus......Page 89 Comments......Page 90 Product of types......Page 91 Sum type......Page 92 Representation of a free structure......Page 93 Free structure......Page 94 Induction......Page 95 Integers......Page 96 Lists......Page 98 Trees of branching type U......Page 100 The Curry-Howard Isomorphism......Page 101 Coherence Semantics of the Sum......Page 102 Lifted sum......Page 103 dI-domains......Page 105 Characterisation in terms of preservation......Page 106 Linear implication......Page 107 Linearisation......Page 108 Linearised sum......Page 110 Tensor product and units......Page 111 The key cases......Page 112 The principal lemma......Page 116 The Hauptsatz......Page 118 Resolution......Page 119 Strong Normalisation for F......Page 121 Remarks......Page 122 Definitions......Page 123 Reducibility with parameters......Page 124 Universal application......Page 125 Reducibility theorem......Page 126 Representation Theorem......Page 127 Numerals......Page 128 Total recursive functions......Page 129 Provably total functions......Page 130 Proofs into programs......Page 131 Formulation of HA2......Page 132 Translation of HA2 into F......Page 133 Representation of provably total functions......Page 134 Proof without undefined objects......Page 136 Finite approximation......Page 139 Saturated domains......Page 140 Uniformity......Page 141 Rigid Embeddings......Page 142 Functoriality of arrow......Page 143 Interpretation of Types......Page 144 Tokens for universal types......Page 145 Linear notation for tokens......Page 146 The three simplest types......Page 147 Variable coherence spaces......Page 148 Coherence of tokens......Page 149 Interpretation of F......Page 151 Of course......Page 152 Natural Numbers......Page 154 Linear numerals......Page 155 Total domains......Page 156 Classical logic is not constructive......Page 157 Linear Sequent Calculus......Page 159 Proof nets......Page 162 Cut elimination......Page 165 Proof nets and natural deduction......Page 168