Types and Programming Languages

Front Cover
MIT Press, Jan 4, 2002 - Computers - 648 pages
9 Reviews
Reviews aren't verified, but Google checks for and removes fake content when it's identified
A comprehensive introduction to type systems and programming languages.

A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems—and of programming languages from a type-theoretic perspective—has important applications in software engineering, language design, high-performance compilers, and security.

This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material.

The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.

 

What people are saying - Write a review

User ratings

5 stars
7
4 stars
1
3 stars
0
2 stars
0
1 star
1

Reviews aren't verified, but Google checks for and removes fake content when it's identified
User Review - Flag as inappropriate

This book is about all the crap-and-crip of programming languages, and it contains some mathematical expressions of programming.

User Review - Flag as inappropriate

Fantastic book. Builds up ideas in a logical manner, and also includes good references for further reading.

Contents

II
1
III
4
IV
9
V
10
VI
12
VII
15
VIII
16
IX
18
CVII
249
CVIII
251
CIX
254
CX
261
CXI
262
CXII
263
CXIII
265
CXIV
267

X
19
XI
20
XII
21
XIII
23
XIV
26
XV
29
XVI
32
XVII
34
XVIII
43
XIX
45
XX
46
XXI
47
XXII
49
XXIII
51
XXIV
52
XXV
58
XXVI
68
XXVII
73
XXVIII
75
XXIX
76
XXX
78
XXXI
80
XXXII
83
XXXIII
85
XXXIV
87
XXXV
88
XXXVI
89
XXXVII
91
XXXVIII
92
XXXIX
95
XL
99
XLI
100
XLII
104
XLIII
108
XLIV
109
XLV
111
XLVII
113
XLVIII
115
L
117
LI
118
LII
119
LIII
121
LIV
124
LV
126
LVI
128
LVII
129
LVIII
132
LIX
136
LX
142
LXI
146
LXII
149
LXIII
152
LXIV
153
LXV
159
LXVII
162
LXVIII
165
LXIX
170
LXX
171
LXXI
172
LXXII
173
LXXIII
175
LXXIV
179
LXXV
181
LXXVIII
182
LXXIX
188
LXXX
191
LXXXI
193
LXXXII
200
LXXXIII
206
LXXXIV
207
LXXXV
209
LXXXVI
210
LXXXVII
213
LXXXVIII
218
LXXXIX
220
XC
221
XCI
222
XCII
225
XCIII
228
XCIV
229
XCVI
230
XCVII
231
XCVIII
233
XCIX
234
CI
235
CII
237
CIII
241
CIV
244
CV
245
CVI
247
CXV
268
CXVI
275
CXVII
279
CXIX
281
CXX
282
CXXI
284
CXXII
286
CXXIII
288
CXXIV
290
CXXV
295
CXXVI
298
CXXVII
299
CXXVIII
304
CXXIX
309
CXXX
311
CXXXI
312
CXXXII
315
CXXXIII
317
CXXXIV
319
CXXXV
321
CXXXVI
326
CXXXVII
329
CXXXVIII
330
CXXXIX
331
CXL
336
CXLI
339
CXLII
340
CXLIII
341
CXLIV
344
CXLV
353
CXLVI
354
CXLVII
357
CXLVIII
358
CXLIX
359
CL
360
CLI
361
CLII
363
CLIII
368
CLIV
377
CLV
379
CLVI
381
CLVII
382
CLVIII
383
CLIX
385
CLX
386
CLXI
389
CLXII
391
CLXIII
396
CLXIV
400
CLXV
406
CLXVI
408
CLXVII
411
CLXVIII
417
CLXIX
418
CLXX
421
CLXXI
424
CLXXII
427
CLXXIII
432
CLXXIV
435
CLXXV
436
CLXXVI
437
CLXXVII
439
CLXXVIII
440
CLXXIX
445
CLXXX
449
CLXXXI
450
CLXXXII
453
CLXXXIII
461
CLXXXIV
462
CLXXXV
467
CLXXXVI
469
CLXXXVII
472
CLXXXIX
475
CXC
476
CXCI
477
CXCII
479
CXCIII
480
CXCIV
481
CXCV
482
CXCVI
485
CXCVII
486
CXCVIII
488
CXCIX
491
CC
493
CCI
565
CCII
566
CCIII
567
CCIV
605
Copyright

Other editions - View all

Common terms and phrases

About the author (2002)

Benjamin C. Pierce is Professor of Computer and Information Science at the University of Pennsylvania.

Bibliographic information