9780262162098

Types and Programming Languages

by
  • ISBN13:

    9780262162098

  • ISBN10:

    0262162091

  • Format: Hardcover
  • Copyright: 2002-02-01
  • Publisher: Mit Pr
  • Purchase Benefits
  • Free Shipping On Orders Over $35!
    Your order must be $35 or more to qualify for free economy shipping. Bulk sales, PO's, Marketplace items, eBooks and apparel do not qualify for this offer.
  • Get Rewarded for Ordering Your Textbooks! Enroll Now
  • We Buy This Book Back!
    In-Store Credit: $8.40
    Check/Direct Deposit: $8.00
    PayPal: $8.00
List Price: $95.00 Save up to $2.85
  • Buy New
    $92.15
    Add to Cart Free Shipping

    SPECIAL ORDER: 1-2 WEEKS

Supplemental Materials

What is included with this book?

  • The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.
  • The eBook copy of this book is not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

Summary

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.

Table of Contents

Preface xiii
Introduction
1(14)
Types in Computer Science
1(3)
What Type Systems Are Good For
4(5)
Type Systems and Language Design
9(1)
Capsule History
10(2)
Related Reading
12(3)
Mathematical Preliminaries
15(6)
Sets, Relations, and Functions
15(1)
Ordered Sets
16(2)
Sequences
18(1)
Induction
19(1)
Background Reading
20(1)
I Untyped Systems 21(68)
Untyped Arithmetic Expressions
23(22)
Introduction
23(3)
Syntax
26(3)
Induction on Terms
29(3)
Semantic Styles
32(2)
Evaluation
34(9)
Notes
43(2)
An ML Implementation of Arithmetic Expressions
45(6)
Syntax
46(1)
Evaluation
47(2)
The Rest of the Story
49(2)
The Untyped Lambda-Calculus
51(24)
Basics
52(6)
Programming in the Lambda-Calculus
58(10)
Formalities
68(5)
Notes
73(2)
Nameless Representation of Terms
75(8)
Terms and Contexts
76(2)
Shifting and Substitution
78(2)
Evaluation
80(3)
An ML Implementation of the Lambda-Calculus
83(6)
Terms and Contexts
83(2)
Shifting and Substitution
85(2)
Evaluation
87(1)
Notes
88(1)
II Simple Types 89(90)
Types Arithmetic Expressions
91(8)
Types
91(1)
The Typing Relation
92(3)
Safety = Progress + Preservation
95(4)
Simply Typed Lambda-Calculus
99(14)
Function Types
99(1)
The Typing Relation
100(4)
Properties of Typing
104(4)
The Curry-Howard Correspondence
108(1)
Erasure and Typability
109(2)
Curry-Style vs. Church-Style
111(1)
Notes
111(2)
An ML Implementation of Simple Types
113(4)
Contexts
113(2)
Terms and Types
115(1)
Typechecking
115(2)
Simple Extensions
117(32)
Base Types
117(1)
The Unit Type
118(1)
Derived Forms: Sequencing and Wildcards
119(2)
Ascription
121(3)
Let Bindings
124(2)
Pairs
126(2)
Tuples
128(1)
Records
129(3)
Sums
132(4)
Variants
136(6)
General Recursion
142(4)
Lists
146(3)
Normalization
149(4)
Normalization for Simple Types
149(3)
Notes
152(1)
References
153(18)
Introduction
153(6)
Typing
159(1)
Evaluation
159(3)
Store Typings
162(3)
Safety
165(5)
Notes
170(1)
Exceptions
171(8)
Raising Exceptions
172(1)
Handling Exceptions
173(2)
Exceptions Carrying Values
175(4)
III Subtyping 179(86)
Subtyping
181(28)
Subsumption
181(1)
The Subtype Relation
182(6)
Properties of Subtyping and Typing
188(3)
The Top and Bottom Types
191(2)
Subtyping and Other Features
193(7)
Coercion Semantics for Subtyping
200(6)
Intersection and Union Types
206(1)
Notes
207(2)
Metatheory of Subtyping
209(12)
Algorithmic Subtyping
210(3)
Algorithmic Typing
213(5)
Joins and Meets
218(2)
Algorithmic Typing and the Bottom Type
220(1)
An ML Implementation of Subtyping
221(4)
Syntax
221(1)
Subtyping
221(1)
Typing
222(3)
Case Study: Imperative Objects
225(22)
What Is Object-Oriented Programming?
225(3)
Objects
228(1)
Object Generators
229(1)
Subtyping
229(1)
Grouping Instance Variables
230(1)
Simple Classes
231(2)
Adding Instance Variables
233(1)
Calling Superclass Methods
234(1)
Classes with Self
234(1)
Open Recursion through Self
235(2)
Open Recursion and Evaluation Order
237(4)
A More Efficient Implementation
241(3)
Recap
244(1)
Notes
245(2)
Case Study: Featherweight Java
247(18)
Introduction
247(2)
Overview
249(2)
Nominal and Structural Type Systems
251(3)
Definitions
254(7)
Properties
261(1)
Encodings vs. Primitive Objects
262(1)
Notes
263(2)
IV Recursive Types 265(50)
Recursive Types
267(14)
Examples
268(7)
Formalities
275(4)
Subtyping
279(1)
Notes
279(2)
Metatheory of Recursive Types
281(34)
Induction and Coinduction
282(2)
Finite and Infinite Types
284(2)
Subtyping
286(2)
A Digression on Transitivity
288(2)
Membership Checking
290(5)
More Efficient Algorithms
295(3)
Regular Trees
298(1)
μ-Types
299(5)
Counting Subexpressions
304(5)
Digression: An Exponential Algorithm
309(2)
Subtyping Iso-Recursive Types
311(1)
Notes
312(3)
V Polymorphism 315(122)
Type Reconstruction
317(22)
Type Variables and Substitutions
317(2)
Two Views of Type Variables
319(2)
Constraint-Based Typing
321(5)
Unification
326(3)
Principal Types
329(1)
Implicit Type Annotations
330(1)
Let-Polymorphism
331(5)
Notes
336(3)
Universal Types
339(24)
Motivation
339(1)
Varieties of Polymorphism
340(1)
System F
341(3)
Examples
344(9)
Basic Properties
353(1)
Erasure, Typability, and Type Reconstruction
354(3)
Erasure and Evaluation Order
357(1)
Fragments of System F
358(1)
Parametricity
359(1)
Impredicativity
360(1)
Notes
361(2)
Existential Types
363(18)
Motivation
363(5)
Data Abstraction with Existentials
368(9)
Encoding Existentials
377(2)
Notes
379(2)
An ML Implementation of System F
381(8)
Nameless Representation of Types
381(1)
Type Shifting and Substitution
382(1)
Terms
383(2)
Evaluation
385(1)
Typing
386(3)
Bounded Quantification
389(22)
Motivation
389(2)
Definitions
391(5)
Examples
396(4)
Safety
400(6)
Bounded Existential Types
406(2)
Notes
408(3)
Case Study: Imperative Objects, Redux
411(6)
Metatheory of Bounded Quantification
417(20)
Exposure
417(1)
Minimal Typing
418(3)
Subtyping in Kernel F<:
421(3)
Subtyping in Full F<:
424(3)
Undecidability of Full F<:
427(5)
Joins and Meets
432(3)
Bounded Existentials
435(1)
Bounded Quantification and the Bottom Type
436(1)
VI Higher-Order Systems 437(54)
Type Operators and Kinding
439(10)
Intuitions
440(5)
Definitions
445(4)
Higher-Order Polymorphism
449(18)
Definitions
449(1)
Example
450(3)
Properties
453(8)
Fragments of Fw
461(1)
Going Further: Dependent Types
462(5)
Higher-Order Subtyping
467(8)
Intuitions
467(2)
Definitions
469(3)
Properties
472(1)
Notes
472(3)
Case Study: Purely Functional Objects
475(16)
Simple Objects
475(1)
Subtyping
476(1)
Bounded Quantification
477(2)
Interface Types
479(1)
Sending Messages to Objects
480(1)
Simple Classes
481(1)
Polymorphic Update
482(3)
Adding Instance Variables
485(1)
Classes with ``Self''
486(2)
Notes
488(3)
Appendices 491(76)
A Solutions to Selected Exercises
493(72)
B Notational Conventions
565(2)
B.1 Metavariable Names
565(1)
B.2 Rule Naming Conventions
565(1)
B.3 Naming and Subscripting Conventions
566(1)
References 567(38)
Index 605

Rewards Program

Write a Review