Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying it in detail. By concentrating on the principles that make the theory work in practice, the author covers all the key ideas without getting involved in the complications of more advanced systems. This book takes a type-assignment approach to type theory, and the system considered is the simplest polymorphic one. The author covers all the basic ideas, including the system's relation to propositional logic, and gives a careful treatment of the type-checking algorithm that lies at the heart of every such system. Also featured are two other interesting algorithms that until now have been buried in inaccessible technical literature. The mathematical presentation is rigorous but clear, making it the first book at this level that can be used as an introduction to type theory for computer scientists.
Author(s): J Roger Hindley
Series: Cambridge Tracts in Theoretical Computer Science 42
Publisher: Cambridge University Press
Year: 1997
Language: English
Pages: 199
City: Cambridge, U.K. ; New York, NY, USA
Contents......Page 8
Introduction......Page 10
A. λ-terms and their structure......Page 14
B. β-reduction and β-normal forms......Page 17
C. η- and βη-reductions......Page 20
D. Restricted λ-terms......Page 23
A. The system TA_λ......Page 25
B. The subject-construction theorem......Page 33
C. Subject reduction and expansion......Page 37
D. The typable terms......Page 40
3. The principal-type algorithm......Page 43
A. Principal types and their history......Page 44
B. Type-substitutions......Page 47
C. Motivating the PT algorithm......Page 51
D. Unification......Page 53
E. The PT algorithm......Page 57
A. The equality rule......Page 65
B. Semantics and completeness......Page 70
A. Typed terms......Page 76
B. Reducing typed terms......Page 80
C. Normalization theorems......Page 84
A. Intuitionist implicational logic......Page 87
B. The Curry-Howard isomorphism......Page 92
C. Some weaker logics......Page 98
D. Axiom-based versions......Page 101
A. The converse PT theorems......Page 106
B. Identifications......Page 108
C. The converse PT proof......Page 109
D. Condensed detachment......Page 115
A. Inhabitants......Page 121
B. Examples of the search strategy......Page 127
C. The search algorithm......Page 131
D. The counting algorithm......Page 137
E. The structure of a nf scheme......Page 140
F. Stretching, shrinking and completeness......Page 145
A. The structure of a term......Page 153
B. Residuals......Page 157
C. The structure of a TA_λ-deduction......Page 161
D. The structure of a type......Page 164
E. The condensed structure of a type......Page 166
F. Imitating combinatory logic in λ-calculus......Page 170
Answers to starred exercises......Page 174
Bibliography......Page 182
Table of principal types......Page 190
Index......Page 192
