Practical Foundations for Programming Languages

This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages and provide the framework for combining and comparing language features. The broad range of concepts includes fundamental data types such as sums and products, polymorphic and abstract types, dynamic typing, dynamic dispatch, subtyping and refinement types, symbols and dynamic classification, parallelism and cost semantics, and concurrency and distribution. The methods are directly applicable to language implementation, to the development of logics for reasoning about programs, and to the formal verification language properties such as type safety. This thoroughly revised second edition includes exercises at the end of nearly every chapter and a new chapter on type refinements.

本書基於類型系統和結構操作語義，發展了一個全面的編程語言理論。語言概念通過它們的靜態和動態語義精確地定義，以直觀和嚴謹的方式呈現基本工具，並僅依賴基礎數學。這些工具用於分析和證明語言的屬性，並提供了結合和比較語言特性的框架。廣泛的概念範圍包括基本數據類型，如和積，多態和抽象類型，動態類型，動態分派，子類型和細化類型，符號和動態分類，並行性和成本語義，以及並發性和分佈性。這些方法直接應用於語言實現，用於開發用於推理程序的邏輯，以及用於形式驗證語言屬性，如類型安全性。這本全面修訂的第二版在幾乎每一章的末尾都包含練習題，並新增了一章關於類型細化。