Computation and Reasoning: A Type Theory for Computer Science

Title page......Page 1
Preface......Page 7
Contents......Page 9
1.1 Motivations in computer science......Page 13
1.2.1 Objects & types......Page 15
1.2.2 Propositions as types......Page 17
1.2.3 Meaning & use......Page 18
1.3 The conceptual universe of types......Page 20
1.3.1 Paradoxical type structures......Page 21
1.3.2 Martin-Löf\'s type theory......Page 22
1.3.3 Impredicative type theories......Page 23
1.3.4 Data types vs. logical propositions......Page 24
1.4 Towards a unifying theory of dependent types......Page 27
2.1.1 Terms & computation......Page 33
2.1.2 Judgements & inference rules......Page 36
2.2.1 Computation & computational equality......Page 38
2.2.2 Judgements & context validity......Page 40
2.2.4 Non-propositional types......Page 41
2.2.5 Predicative universes & the reflection principle......Page 44
2.2.6 Propositions & the impredicative universe......Page 46
2.2.7 Type equality & the cumulativity relation......Page 48
2.3.1 Data types vs. logical propositions......Page 50
2.3.2 Sigma-types & existential types......Page 53
2.3.3 Equalities: intensionality vs. extensionality......Page 55
2.3.5 On the use of the type theory......Page 58
3.1 Church-Rosser theorem & cumulativity......Page 61
3.2 Derivable judgements & derivability......Page 66
3.3 Principal types......Page 73
4 Strong normalisation......Page 77
4.1.1 The reducibility method & the notion of predicativity......Page 78
4.1.2 Environments......Page 81
4.1.3 Saturated sets & candidates of reducibility......Page 83
4.2.1 Levels of types......Page 86
4.2.2 Quasi-normalisation & degrees of types......Page 88
4.2.3 The complexity measure of types......Page 91
4.2.4 An inductive proof of the quasi-normalisation theorem......Page 93
4.3.1 Possible denotations of objects......Page 100
4.3.2 Assignments & valuations......Page 102
4.3.3 The interpretation......Page 104
4.3.4 Soundness of the interpretation......Page 108
4.3.5 The strong normalisation theorem......Page 112
5.1.1 The internal logic & its consistency......Page 115
5.1.2 Understanding the logical operators......Page 118
5.1.3 The Leibniz equality & equality reflection......Page 121
5.2.2 Decidability of type inference & type checking......Page 124
6 A set-theoretic model......Page 129
6.1 Understanding ECC in the Omega-Set framework......Page 130
6.2 Valid contexts & objects......Page 132
6.3 Predicative universes & non-propositional types......Page 133
6.4 The impredicative universe & propositions......Page 135
6.5 Remarks......Page 137
7 Computational & logical theories......Page 139
7.1.1 The type of natural numbers......Page 140
7.1.2 The type of lists of natural numbers......Page 143
7.2 Abstract theories & abstract reasoning......Page 144
7.2.1 A notion of abstract theory......Page 145
7.2.3 Theory morphisms & proof inheritance......Page 148
7.3 Discussion......Page 149
8 Specification & development of programs......Page 151
8.1 A brief summary......Page 152
8.2.1 Program specifications & their realisations......Page 153
8.2.2 Specifications of abstract data types......Page 156
8.2.3 Data refinement & implementation......Page 158
8.3 Modular design & structured specification......Page 161
8.3.1 Decomposition & sharing......Page 162
8.3.2 Constructors & selectors......Page 165
8.4 Parameterised specification......Page 168
8.4.1 Parameterised specifications......Page 169
8.4.2 Implementation of parameterised specifications......Page 171
8.5 Discussion......Page 174
9 Towards a unifying theory of dependent types......Page 177
9.1.1 Martin-Löf\'s logical framework......Page 178
9.1.2 Specifying type theories in LF......Page 182
9.1.3 Inductive schemata......Page 185
9.2.1 SOL: the internal logical mechanism......Page 187
9.2.2 Inductive data types......Page 189
9.2.3 Predicative universes......Page 194
9.2.4 A summary......Page 197
9.3.1 The internal logic & pure logical truths......Page 198
9.3.2 Further separation of propositions & data types......Page 207
9.3.3 Intensionality & Eta-equality rules......Page 210
9.3.4 Understanding of the type theory......Page 214
9.3.5 Inductive families of types......Page 216
9.3.6 Subtyping & other implementation issues......Page 220
9.4 Final remarks......Page 221
Bibliography......Page 223
Notation & Symbols......Page 233
Index......Page 237