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.
Author(s): Jean-Yves Girard, Yves Lafont, Paul Taylor
Series: Cambridge Tracts in Theoretical Computer Science 7
Publisher: Cambridge University Press
Year: 1989
Language: English
Pages: 175
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
