型とプログラム言語:テキスト<br>Types and Programming Languages

個数:

型とプログラム言語:テキスト
Types and Programming Languages

  • 提携先の海外書籍取次会社に在庫がございます。通常2週間で発送いたします。
    重要ご説明事項
    1. 納期遅延や、ご入手不能となる場合が若干ございます。
    2. 複数冊ご注文の場合、分割発送となる場合がございます。
    3. 美品のご指定は承りかねます。

  • 提携先の海外書籍取次会社に在庫がございます。通常約2週間で発送いたします。
    重要ご説明事項
    1. 納期遅延や、ご入手不能となる場合が若干ございます。
    2. 複数冊ご注文の場合、分割発送となる場合がございます。
    3. 美品のご指定は承りかねます。
  • 製本 Hardcover:ハードカバー版/ページ数 623 p.
  • 言語 ENG,ENG
  • 商品コード 9780262162098
  • DDC分類 005.13

基本説明

This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. Contents: Untyped Systems; Simple Types; Subtyping; Recursive Types; Polymorphism; Higher-Order Systems.

Full Description


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.

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