Type Systems Notes

Master

Preliminary sketch, based on referenced book.

A selection from the content taken from book (see Material, or http://www.cis.upenn.edu/~bcpierce/tapl).

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
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
- 26 Bounded Quantication 389
- 27 Case Study: Imperative Objects, Redux 411
- 28 Metatheory of Bounded Quantication 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

and

none