History of Lambda-calculus and Combinatory Logic
Felice Cardone, Roger Hindley · 2006
8 Types 23 8.1 The general development of type theories . . . . . . . . . . . . . . . 23 8.1.1 Types as grammatical categories . . . . . . . . . . . . . . . . 24 8.1.2 Types as sets . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 8.1.3 Types as objects . . . . . . . . . . . . . . . . . . . . . . . . . 26 8.1.4 Types as propositions . . . . . . . . . . . . . . . . . . . . . . 30 8.2 Early normalization proofs . . . . . . . . . . . . . . . . . . . . . . . . 35 8.3 Higher-order type theories . . . . . . . . . . . . . . . . . . . . . . . . 37