Proofs and Types

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