This book develops a type theory, studies its properties, and explains its uses in computer science. The book focuses in particular on how the study of type theory may offer a powerful and uniform language for programming, program specification and development, and logical reasoning. The type theory developed here reflects a conceptual distinction between logical propositions and computational data types. Starting from an introduction of the basic concepts, the author explains the meaning and use of the type-theoretic language with proof-theoretic justifications, and discusses various issues in the study of type theory. The practical use of the language is illustrated by developing an approach to specification and data refinement in type theory, which supports modular development of specification, programs, and proofs. Students and researchers in computer science and logic will welcome this exciting new book.
Author(s): Zhaohui Luo
Series: International Series of Monographs on Computer Science 11
Publisher: Oxford University Press, USA
Year: 1994
Language: English
Pages: 240
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
