Types and Programming Languages > 프로그래밍

Preface
1 Introduction 1
2 Mathematical Preliminaries 15
I Untyped Systems 21
3 Untyped Arithmetic Expressions 23
4 An ML Implementation of Arithmetic Expressions 45
5 The Untyped Lambda-Calculus 51
6 Nameless Representation of Terms 75
7 An ML Implementation of the Lambda-Calculus 83
II Simple Types 89
8 Typed Arithmetic Expressions 91
9 Simply Typed Lambda-Calculus 99
10 An ML Implementation of Simple Types 113
11 Simple Extensions 117
12 Normalization 149
13 References 153
14 Exceptions 171
III Subtyping 179
15 Subtyping 181
16 Metatheory of Subtyping 209
17 An ML Implementation of Subtyping 221
18 Case Study: Imperative Objects 225
19 Case Study: Featherweight Java 247
IV Recursive Types 265
20 Recursive Types 267
21 Metatheory of Recursive Types 281
V Polymorphism 315
22 Type Reconstruction 317
23 Universal Types 339
24 Existential Types 363
25 An ML Implementation of System F 381
26 Bounded Quantification 389
27 Case Study: Imperative Objects, Redux 411
28 Metatheory of Bounded Quantification 417
VI Higher-Order Systems 437
29 Type Operators and Kinding 439
30 Higher-Order Polymorphism 449
31 Higher-Order Subtyping 467
32 Case Study: Purely Functional Objects 475
Appendices 491
A: Solutions to Selected Exercises 493
B: Notational Conventions 565
References 567
Index 605