Advanced Topics In Types And Programming Languages

by Pierce, Benjamin C.

• ISBN13: 9780262162289
• ISBN10: 0262162288
• Format: Hardcover
• Copyright: 2004-12-23
• Publisher: The MIT Press

Summary

The study of type systems for programming languages now touches many areas of computer science, from language design and implementation to software engineering, network security, databases, and analysis of concurrent and distributed systems. This book offers accessible introductions to key ideas in the field, with contributions by experts on each topic. The topics covered include precise type analyses, which extend simple type systems to give them a better grip on the run time behavior of systems; type systems for low-level languages; applications of types to reasoning about computer programs; type theory as a framework for the design of sophisticated module systems; and advanced techniques in ML-style type inference. Advanced Topics in Types and Programming Languagesbuilds on Benjamin Pierce's Types and Programming Languages(MIT Press, 2002); most of the chapters should be accessible to readers familiar with basic notations and techniques of operational semantics and type systems -- the material covered in the first half of the earlier book. Advanced Topics in Types and Programming Languagescan be used in the classroom and as a resource for professionals. Most chapters include exercises, ranging in difficulty from quick comprehension checks to challenging extensions, many with solutions.

Author Biography

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

Table of Contents

Preface	ix
I Precise Type Analyses	1	(136)
Substructural Type Systems	3	(42)
David Walker
Structural Properties	4	(2)
A Linear Type System	6	(11)
Extensions and Variations	17	(13)
An Ordered Type System	30	(6)
Further Applications	36	(4)
Notes	40	(5)
Dependent Types	45	(42)
David Aspinall
Martin Hofmann
Motivations	45	(5)
Pure First-Order Dependent Types	50	(4)
Properties	54	(2)
Algorithmic Typing and Equality	56	(5)
Dependent Sum Types	61	(3)
The Calculus of Constructions	64	(7)
Relating Abstractions: Pure Type Systems	71	(3)
Programming with Dependent Types	74	(9)
Implementation of Dependent Types	83	(3)
Further Reading	86	(1)
Effect Types and Region-Based Memory Management	87	(50)
Fritz Henglein
Henning Makholm
Henning Niss
Introduction and Overview	87	(3)
Value Flow by Typing with Labels	90	(12)
Effects	102	(4)
Region-Based Memory Management	106	(8)
The Tofte-Talpin Type System	114	(9)
Region Inference	123	(4)
More Powerful Models for Region-Based Memory Management	127	(6)
Practical Region-Based Memory Management Systems	133	(4)
II Types for Low-Level Languages	137	(84)
Typed Assembly Language	141	(36)
Greg Morrisett
TAL-0: Control-Flow-Safety	142	(4)
The TAL-0 Type System	146	(9)
TAL-1: Simple Memory-Safety	155	(6)
TAL-1 Changes to the Type System	161	(3)
Compiling to TAL-1	164	(3)
Scaling to Other Language Features	167	(5)
Some Real World Issues	172	(3)
Conclusions	175	(2)
Proof-Carrying Code	177	(44)
George Necula
Overview of Proof Carrying Code	177	(5)
Formalizing the Safety Policy	182	(5)
Verification-Condition Generation	187	(12)
Soundness Proof	199	(5)
The Representation and Checking of Proofs	204	(10)
Proof Generation	214	(2)
PCC beyond Types	216	(3)
Conclusion	219	(2)
III Types and Reasoning about Programs	221	(70)
Logical Relations and a Case Study in Equivalence Checking	223	(22)
Karl Crary
The Equivalence Problem	224	(1)
Non-Type-Directed Equivalence Checking	225	(2)
Type-Driven Equivalence	227	(1)
An Equivalence Algorithm	228	(4)
Completeness: A First Attempt	232	(1)
Logical Relations	233	(3)
A Monotone Logical Relation	236	(1)
The Main Lemma	237	(2)
The Fundamental Theorem	239	(4)
Notes	243	(2)
Typed Operational Reasoning	245	(46)
Andrew Pitts
Introduction	245	(1)
Overview	246	(1)
Motivating Examples	247	(6)
The Language	253	(8)
Contextual Equivalence	261	(5)
An Operationally Based Logical Relation	266	(13)
Operational Extensionality	279	(9)
Notes	288	(3)
IV Types for Programming in the Large	291	(96)
Design Considerations for ML-Style Module Systems	293	(54)
Robert Harper
Benjamin C. Pierce
Basic Modularity	294	(4)
Type Checking and Evaluation of Modules	298	(4)
Compilation and Linking	302	(3)
Phase Distinction	305	(2)
Abstract Type Components	307	(10)
Module Hierarchies	317	(3)
Signature Families	320	(4)
Module Families	324	(14)
Advanced Topics	338	(3)
Relation to Some Existing Languages	341	(2)
History and Further Reading	343	(4)
Type Definitions	347	(40)
Christopher A. Stone
Definitions in the Typing Context	351	(7)
Definitions in Module Interfaces	358	(9)
Singleton Kinds	367	(17)
Notes	384	(3)
V Type Inference	387	(104)
The Essence of ML Type Inference	389	(102)
Francois Pottier
Didier Remy
What Is ML?	389	(18)
Constraints	407	(15)
HM(X)	422	(7)
Constraint Generation	429	(5)
Type Soundness	434	(4)
Constraint Solving	438	(13)
From ML-the-Calculus to ML-the-Language	451	(9)
Rows	460	(31)
A Solutions to Selected Exercises	491	(44)
References	535	(32)
Index	567