Advanced Topics in Types and Programming Languages (Hardcover) (進階類型與程式語言主題)

Benjamin C. Pierce

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. 低級語言的類型

類似商品