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.

这篇文章在类型系统和结构性操作语义的基础上发展了一套全面的编程语言理论。语言概念由其静态和动态语义精确定义，在只依赖基本数学的情况下，直观和严格地介绍了基本工具。这些工具被用来分析和证明语言的属性，并为组合和比较语言特征提供框架。广泛的概念包括基本数据类型，如和与积，多态和抽象类型，动态类型，动态调度，子类型和细化类型，符号和动态分类，并行和成本语义，以及并发和分布。这些方法直接适用于语言的实现，用于推理程序的逻辑学的发展，以及形式化验证语言的属性，如类型安全。这个彻底修订的第二版包括几乎每一章末尾的练习和关于类型细化的新章节。