Types and Programming Languages

Přední strana obálky
MIT Press, 4. 1. 2002 - Počet stran: 648
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.

 

Obsah

Introduction
1
Mathematical Preliminaries
15
Untyped Arithmetic Expressions
23
Implementation of Arithmetic Expressions
45
The Untyped LambdaCalculus
51
Nameless Representation of Terms
75
An ML Implementation of the LambdaCalculus
83
Typed Arithmetic Expressions
91
Type Reconstruction
317
Universal Types
339
Existential Types
363
An ML Implementation of System F
381
Bounded Quantification
389
Imperative Objects Redux
411
Metatheory of Bounded Quantification
417
Type Operators and Kinding
439

Simply Typed LambdaCalculus
99
An ML Implementation of Simple Types
113
Normalization
149
Exceptions
171
Subtyping
181
Metatheory of Subtyping
209
An ML Implementation of Subtyping
221
Featherweight Java
247
Recursive Types
267
Metatheory of Recursive Types
281
HigherOrder Polymorphism
449
HigherOrder Subtyping
467
Purely Functional Objects
475
A Solutions to Selected Exercises
493
B Notational Conventions
565
113
584
115
602
Index
605
Autorská práva

Další vydání - Zobrazit všechny

Types and Programming Languages
Benjamin C. Pierce
Omezený náhled - 2002
Types and Programming Languages
Benjamin C. Pierce
Omezený náhled - 2002
Types and Programming Languages
Benjamin C. Pierce
Náhled není k dispozici. - 2002

Běžně se vyskytující výrazy a sousloví

abstraction actually algorithm allow annotations apply argument base behavior binding body Bool booleans bound calculate called Chapter computation conditional consider construct constructor contains context corresponding Counter defined definition derivation elements encoding error evaluation evaluation rules example exception EXERCISE existential expressions extend fact false field Figure final follows formal function give given implementation induction induction hypothesis instance introduced intuition Java kind lambda-calculus language lemma List match methods names Note numbers object obtain operations pair polymorphism premise present programming proof prove record recursive reference relation representation represented result returns semantics sequence similar simply simply typed SOLUTION statement step structure substitution subtype relation subtyping succ Suppose syntax term THEOREM tion tree true type systems type variables typechecking typing rules unit variables variant write written yields

O autorovi (2002)

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

Bibliografické údaje

NázevTypes and Programming Languages
AutorBenjamin C. Pierce
VydavatelMIT Press, 2002
ISBN0262303825, 9780262303828
DélkaPočet stran: 648
  
Exportovat citaciBiBTeX EndNote RefMan