Advanced Topics in Types and Programming Languages (Hardcover)

Description:

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 Languages builds 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 Languages can 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.

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
1	Substructural Type Systems David Walker	3
2	Dependent Types David Aspinall and Martin Hofmann	45
II	Types for Low-Level Languages	137
4	Typed Assembly Language Greg Morrisett	141
5	Proof-Carrying Code George Necula	177
III	Types and Reasoning about Programs	221
6	Logical Relations and a Case Study in Equivalence Checking Karl Crary	223
7	Typed Operational Reasoning Andrew Pitts	245
IV	Types for Programming in the Large	291
8	Design Considerations for ML-Style Module Systems Robert Harper and Benjamin C. Pierce	293
9	Type Definitions Christopher Stone	347
V	Type Inference	387
10	The Essence of ML Type Inference François Pottier and Didier Rémy	389
A	Solutions to Selected Exercises	491
	References	535
	Index	567

描述：
編程語言的類型系統研究現在涉及計算機科學的許多領域，從語言設計和實現到軟件工程、網絡安全、數據庫以及並發和分佈系統的分析。本書提供了對該領域的關鍵思想的易於理解的介紹，每個主題都由專家提供貢獻。

所涵蓋的主題包括精確的類型分析，它們擴展了簡單的類型系統，以更好地掌握系統的運行時行為；低級語言的類型系統；將類型應用於對計算機程序的推理；類型理論作為設計複雜模塊系統的框架；以及ML風格類型推斷的高級技術。

《類型和編程語言的高級主題》是基於本傑明·皮爾斯（Benjamin Pierce）的《類型和編程語言》（MIT Press，2002）的基礎上建立的；大多數章節對於熟悉操作語義和類型系統的基本符號和技術的讀者來說應該是可理解的 - 這是早期書籍的前半部分所涵蓋的內容。

《類型和編程語言的高級主題》可用於課堂教學和專業人士的資源。大多數章節包括練習題，難度從快速理解檢查到具有挑戰性的擴展，其中許多有解答。

本傑明·C·皮爾斯（Benjamin C. Pierce）是賓夕法尼亞大學計算機和信息科學教授。

目錄：
前言
I. 精確的類型分析
1. 子結構類型系統 - 大衛·沃克
2. 依賴類型 - 大衛·阿斯皮納爾和馬丁·霍夫曼
II. 低級語言的類型
3. 高級主題中的類型和編程語言建立在本傑明·皮爾斯的《類型和編程語言》（MIT Press，2002）的基礎上；大多數章節對於熟悉操作語義和類型系統的基本符號和技術的讀者來說應該是可理解的 - 這是早期書籍的前半部分所涵蓋的內容。

《類型和編程語言的高級主題》可用於課堂教學和專業人士的資源。大多數章節包括練習題，難度從快速理解檢查到具有挑戰性的擴展，其中許多有解答。

本傑明·C·皮爾斯（Benjamin C. Pierce）是賓夕法尼亞大學計算機和信息科學教授。

目錄：
前言
I. 精確的類型分析
1. 子結構類型系統 - 大衛·沃克
2. 依賴類型 - 大衛·阿斯皮納爾和馬丁·霍夫曼
II. 低級語言的類型