English
Programming language theory studies the rules that give programs meaning and the properties those rules support. Syntax determines which expressions can be formed; semantics determines their behavior. A language implementation is evidence about one implementation, not automatically the definition of every behavior the language permits.
Consider replacing f() + f() with 2 * f(). Over suitable arithmetic, the transformation is reasonable if f is pure and terminates with the same value each time. It can change behavior if f advances an input stream, updates state, or raises an exception. Formal semantics makes those distinctions available for a correctness argument instead of leaving them implicit in an optimization.
Start with experience in one language, functions and state, and induction (§2.2). Small calculi isolate one feature at a time. Their purpose is not to reproduce an entire production language immediately, but to make a design choice and its consequences manageable.
How Giving Meaning to Programs Became a Mathematical Discipline
Logic supplied lambda calculus and combinatory logic before electronic programming became an established practice. Programming language design then supplied new questions about assignment, scope, evaluation order, and interaction. The relationship was reciprocal: languages borrowed mathematical structures, while real programs demanded richer models.
ALGOL made the distinction between syntax and semantics especially visible. Its grammar could be presented formally while much of its behavior still required prose. Landin connected programming constructs to lambda calculus and abstract machines. Scott and Strachey’s denotational work supplied mathematical domains in which recursion and partial results could be modeled, rather than treating every program as a total mathematical function.
Floyd and Hoare developed assertion-based reasoning; Plotkin’s structural operational semantics organized execution rules around program syntax. ML’s polymorphic inference showed how types could aid programming without requiring an annotation at every expression. These were complementary responses to the need to understand programs compositionally: reason about a part using the rules governing its parts.
Later work on effects, concurrency, abstraction, and separation logic expanded which observations and resources a model could represent. Mechanized metatheory and verified compilers made the semantic definitions themselves usable software artifacts. The lasting achievement is the ability to state exactly what a translation, optimization, or type discipline preserves—not a claim that every language shares one simple semantics.
Meaning, Equivalence, and Type Soundness
Three questions recur: what executions are permitted, when are two programs interchangeable, and which failures are excluded by a static discipline? They require a common account of observations. Return values alone may suffice for pure expressions; state, exceptions, interaction, and termination can matter elsewhere.
Ways to Define and Compare Program Behavior
Operational semantics describes evaluation through rules for transitions or completed evaluations. Denotational semantics assigns mathematical meanings compositionally: a compound expression’s meaning is built from those of its parts. The chosen domain may represent partiality or effects; nontermination is not always adequately modeled by one undifferentiated value when ongoing interaction is observable.
For x := x+1, an operational rule updates the current store; a denotational account can assign a function that maps an input store to the updated store. These describe what the command does. Axiomatic semantics describes guarantees through assertions: {x=4} x:=x+1 {x=5} records one property of that transformation over mathematical integers. In partial-correctness Hoare logic, {P} C {Q} says that starting in P, any terminating execution of C ends in Q. Total correctness also requires termination. A weakest precondition for total correctness must guarantee that termination; a weakest liberal precondition addresses partial correctness. For the integer command x:=x+1 and desired result x≥0, the weakest precondition is x≥−1: substituting the assigned expression into the desired condition gives x+1≥0. Loops need an additional invariant and, for total correctness, a termination argument. This calculation shows how a postcondition can guide reasoning backward through a program.
Contextual equivalence asks whether any permitted surrounding program can distinguish two components using the selected observations. Equal denotations imply contextual equivalence in an appropriate sound compositional model; the converse is an additional property, called full abstraction. It does not hold automatically for every denotational model. Bisimulation supplies another technique, comparing the steps two systems can match.
Separation logic extends assertion-based reasoning about memory. Its separating conjunction describes disjoint portions of a heap, and a frame rule allows a local proof to carry along untouched resources under its side conditions. For example, if a command changes only a cell at address p, a proof about that cell can carry along an assertion about a disjoint cell at q. The disjointness condition excludes aliasing between them. The frame rule makes explicit why changing one part of memory preserves the assertion about the other.
Recursion explains why denotational models need more than ordinary total functions. One approach begins with an undefined approximation and unfolds the recursive definition repeatedly. For factorial, the first unfolding can define the result at zero, a later one at one, and so on. In suitable ordered domains, the limit of these increasingly informative approximations supplies a least fixed point. The domain and continuity conditions justify that construction; the fixed-point equation alone need not select the intended meaning.
Type Systems and Soundness
A type system classifies expressions and rejects certain combinations before execution. For many small calculi, soundness is proved through progress—a closed well-typed expression is a value or can step—and preservation—a step preserves its type. Together they exclude the designated stuck states. They do not automatically exclude nontermination, handled exceptions, or a result that is wrong for the user’s purpose.
Type inference reconstructs missing type information. Hindley–Milner inference combines unification with let-polymorphism and provides principal types in its setting. Unification solves equalities between unknown types: if integer addition is the only + operation, λx. x+1 forces the parameter and result to be integers. By contrast, a let-bound identity function can have the general type A → A, instantiated separately when applied to an integer and a Boolean. A principal type captures the most general typing from which the permitted instances follow. It is often effective in practice, but general worst-case inference is not polynomial-time; repeated polymorphic use can create very large types. Cornell’s account distinguishes practical behavior from this complexity bound. Richer features can require annotations or a different algorithm.
Parametricity constrains polymorphic behavior under specified semantics. In a pure, total parametric calculus, a closed term of type ∀A. A → A must return its argument. With general recursion it might diverge; with effects it may also do other observable work. A useful “free theorem” states its assumptions rather than treating every generic function in every language as a constructive proof.
Operational Techniques: Big Steps and Small Steps
Small-step semantics records e → e′, one transition at a time. Big-step semantics records e ⇓ v, a completed evaluation. Ordinary inductive big-step rules may assign no result both to divergence and to a stuck term; distinguishing them requires additional judgments or a different formulation. Small-step traces make infinite execution and interleaving easier to describe.
Evaluation order has consequences even without mutable state. The notation λx. e means a function with parameter x and body e; applying it substitutes the argument according to the evaluation rules. Let Ω denote a diverging computation. In (λx. 1) Ω, call-by-value evaluates the argument first and diverges; call-by-name can return 1 because the argument is unused. Call-by-need additionally shares evaluated results. Evaluation contexts specify where the next reduction may occur; they are a compact way to make such choices explicit.
When adding a language feature, ask what rules change and what earlier theorem must be revisited. References, exceptions, and concurrency can invalidate an argument proved only for a pure terminating core. The added feature must be included in the rules before the old guarantee can be claimed for the extended language.
What Studying This Changes
The practical gain is a vocabulary for comparing behavior. Before a refactoring, state which observations must remain unchanged. Before relying on a type error to rule out a bug, identify the property the type system actually enforces. Before treating a compiler optimization as algebra, account for arithmetic and effects.
A useful exercise is to define a tiny expression language, write an evaluator and a few inference rules, then add one feature such as exceptions. Compare the new rules with the old progress or equivalence argument. This connects formal notation to a concrete design decision without requiring a full compiler or proof assistant first.
Resources
Books and Texts
Pierce’s Types and Programming Languages (TAPL, 2002) develops typed lambda calculi, subtyping, recursive types, and polymorphism through formal rules, examples, and proofs. It assumes comfort with induction and mathematical notation. Work through small typing derivations and preservation arguments before moving to richer systems. Advanced Topics in Types and Programming Languages (ATTAPL, 2005) collects further treatments, including dependent types, effects, and typed low-level programming.
Harper’s Practical Foundations for Programming Languages (PFPL, 2nd ed., Cambridge, 2016, draft free online) covers broader ground than TAPL — it includes imperative features, concurrency, and a more complete treatment of advanced type theory — but with denser writing. PFPL is organized around “abstract binding trees,” a formalism for reasoning about syntax with binding that is more general than the presentations in TAPL. Readers willing to invest in the denser presentation get a more complete and contemporary picture of the field.
Winskel’s The Formal Semantics of Programming Languages (1993) develops operational semantics, domain theory, and denotational semantics. It is useful when the main question is how to give meaning to programs and relate different descriptions of behavior. Pair its definitions with small evaluators and store-transforming examples.
Friedman and Wand’s Essentials of Programming Languages (EOPL, 3rd ed., MIT Press, 2008) approaches the material through implementation: readers build interpreters for languages of increasing complexity, and the type systems and semantic concepts are introduced in the context of working implementations. EOPL is more accessible to readers who find the formal texts too abstract initially, and it makes the connection between theory and implementation explicit. For readers who struggle with TAPL’s pace, EOPL first then TAPL is a productive route.
Krishnamurthi’s Programming Languages: Application and Interpretation (PLAI, free online; optional paid print) is another implementation-first route, using interpreters and language variation to make semantic ideas concrete. It is less mathematically deep than TAPL and PFPL, but it is one of the best bridges for programmers who need to build languages before they can comfortably prove things about them.
Reynolds’s Theories of Programming Languages (1998) provides a detailed treatment of language semantics and program reasoning. For separation logic specifically, use his later 2002 paper, rather than attributing that later development to the 1998 book.
For proof assistant-based programming language theory, Pierce et al.’s Software Foundations series (free at softwarefoundations.cis.upenn.edu) provides structured exercises. Volume 1 (Logical Foundations) teaches Coq while introducing logic and proof; Volume 2 (Programming Language Foundations) formalizes operational semantics, type systems, and Hoare logic in Coq. The series is the standard treatment of PLT in mechanized form and is increasingly required reading for anyone who intends to do formal verification work.
For process calculi and concurrent languages, Milner’s Communicating and Mobile Systems: the Pi-Calculus (Cambridge, 1999) is the primary source for the pi-calculus, and Sangiorgi and Walker’s The Pi-Calculus: A Theory of Mobile Processes (Cambridge, 2001) is the comprehensive reference.
| Book | Role | Type |
|---|---|---|
| Pierce, Types and Programming Languages (TAPL) | Canonical entry; type systems | Entry |
| Pierce (ed.), Advanced Topics in Types and Programming Languages (ATTAPL) | Extension of TAPL | Depth |
| Harper, Practical Foundations for Programming Languages (PFPL, draft free) | Broader comprehensive alternative | Depth |
| Winskel, The Formal Semantics of Programming Languages | Operational and denotational semantics | Depth |
| Friedman & Wand, Essentials of Programming Languages (EOPL) | Implementation-first accessible entry | Practice |
| Krishnamurthi, PLAI (free; optional paid print) | Implementation-first PL concepts | Entry |
| Reynolds, Theories of Programming Languages | Denotational + axiomatic at depth | Depth |
| Pierce et al., Software Foundations Vols. 1–2 (free) | Mechanized PLT in Coq | Practice |
| Milner, Communicating and Mobile Systems | Pi-calculus primary source | Depth |
Courses and Lectures
Penn CIS 500 (Software Foundations, Benjamin Pierce, free materials) is the course that TAPL was written for. Complete lecture slides and supplementary materials are freely available. Pierce’s teaching integrates the formal material with programming exercises, and the course structure reveals the pedagogical approach behind the textbook.
Carnegie Mellon 15-312 (Principles of Programming Languages, Robert Harper, free materials) uses PFPL and is Harper’s primary teaching vehicle. His lecture notes develop the material with characteristic directness and are worth reading alongside or instead of PFPL for specific topics.
Oregon Programming Languages Summer School (OPLSS), held annually in Eugene, archives lecture series freely on YouTube. OPLSS attracts leading researchers and the lecture series covers topics from introductory PLT through the research frontier. Specific lecture series to prioritize: Frank Pfenning on proof theory and type theory; Andrew Pitts on nominal techniques; Paul-André Melliès on linear logic and game semantics.
Software Foundations exercises in Coq, available at softwarefoundations.cis.upenn.edu, constitute a self-paced course that develops mechanized proof skills alongside PLT content. Working through Volume 2 produces both PLT knowledge and Coq competence simultaneously.
| Course | Platform | Type |
|---|---|---|
| Penn CIS 500 Software Foundations (Pierce, free) | Penn course site | Entry |
| CMU 15-312 Principles of PL (Harper, free) | CMU course site | Depth |
| OPLSS lectures (free) | YouTube / OPLSS site | Reference |
| Software Foundations exercises in Coq (free) | softwarefoundations.cis.upenn.edu | Practice |
Practice, Tools, and Current Sources
Practice by writing a small-step reduction sequence and a typing derivation for the same expression. Then change one language rule and identify which derivations still hold. This connects inference rules to the behavior they describe.
PLT Redex is a Racket-based environment for specifying and testing operational semantics. Its associated book, Semantics Engineering with PLT Redex, is by Felleisen, Findler, and Flatt. Implement a small expression language, inspect reduction traces, and use generated tests to look for counterexamples to proposed properties. Testing the model complements a proof of its general properties.
Andrej Bauer and Matija Pretnar’s Programming Languages Zoo (free) is a collection of miniature languages demonstrating parsing, interpreters, compilers, static and dynamic typing, subtyping, polymorphism, lazy evaluation, exceptions, and abstract machines. It is especially useful after a reader has learned the concepts and wants to see compact implementations side by side.
Rocq/Coq, Lean, or Agda can check a formalized type-soundness argument. Choose a tutorial that matches the tool and language version. Software Foundations supplies a structured path through progress, preservation, and Hoare logic; the proof state makes missing cases and assumptions visible.
The POPLmark Challenge (poplmark.org) proposed benchmark proofs for PLT metatheory in 2005; the solutions in various proof assistants are freely available and serve as worked examples of mechanized PLT.
| Resource | Platform | Type |
|---|---|---|
| PLT Redex (free) | Racket / racket-lang.org | Practice |
| Programming Languages Zoo (free) | plzoo.andrej.com | Practice |
| Software Foundations in Coq (free) | softwarefoundations.cis.upenn.edu | Practice |
| POPLmark challenge solutions (free) | poplmark.org | Practice |
| Lean 4 / Mathlib PLT formalizations (free) | leanprover-community.github.io | Reference |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Equating implementation behavior with specification | One implementation may choose among permitted behaviors or contain a bug. | Separate the language rules from observations of a particular implementation. |
| Reading “well typed” as “correct” | Soundness excludes specified failures, not every unwanted outcome. | Name the stuck states, effects, and termination assumptions. |
| Treating algebraic rewrites as universally valid | Evaluation order, overflow, and effects can change observations. | State the semantic model before proving an optimization. |
| Assuming equal denotations characterize every equivalence | Full abstraction is an additional property of a model. | Specify contextual observations and which implication has been proved. |
| Assuming decidable inference is always fast | A terminating algorithm can have a high worst-case cost. | Distinguish inference, checking, and the size of inferred types. |
| Transporting a pure-language theorem into an effectful language | Extra operations can violate the theorem’s premises. | Recheck the argument when the language or observation model changes. |
中文
编程语言理论研究赋予程序含义的规则，以及这些规则支持的性质。语法决定哪些表达式可以构成，语义决定它们的行为。某个语言实现提供的是关于该实现的证据，不会自动成为语言允许的全部行为的定义。
考虑把 f() + f() 改成 2 * f()。在适当的算术模型下，如果 f 是纯函数，且每次都终止并返回相同值，这种变换很合理。但如果 f 读取下一项输入、修改状态或抛出异常，行为就可能改变。形式语义使这些区别能够进入正确性论证，而不是隐含在优化中。
从一种语言的使用经验、函数与状态，以及归纳法开始（§2.2）。小型演算每次分离出一种特性。目的不是立即复刻整门生产语言，而是把设计选择及其后果控制在可以理解的范围内。
给程序赋予意义如何成为一门数学学科
在电子编程成为成熟实践之前，逻辑已经提供了 lambda 演算与组合子逻辑。语言设计随后带来了赋值、作用域、求值顺序和交互等新问题。这种关系是双向的：语言借用数学结构，真实程序也要求更丰富的模型。
ALGOL 尤其清楚地显示了语法与语义的区别。文法可以形式化呈现，许多行为却仍需散文说明。Landin 把编程构造连接到 lambda 演算与抽象机器。Scott 和 Strachey 的指称工作提供了数学域，使递归与部分结果能够得到建模，而不把每个程序都当成数学上的全函数。
Floyd 和 Hoare 发展了基于断言的推理；Plotkin 的结构化操作语义围绕程序语法组织执行规则。ML 的多态类型推断表明，类型可以帮助编程，而不要求每个表达式都附带注解。这些方法共同回应了组合式理解的需要：根据组成部分及其组织规则，推理整体。
后来的副作用、并发、抽象与分离逻辑研究，扩展了模型能够表示的观察和资源。机械化元理论与已验证编译器，使语义定义本身也成为可使用的软件产物。持久的成果，是能准确陈述翻译、优化或类型约束保留了什么，而不是声称所有语言都共享一种简单语义。
意义、等价性与类型可靠性
三个问题反复出现：允许哪些执行，两个程序何时可以互换，以及静态约束排除了哪些失败？它们需要共同的观察定义。纯表达式可能只需比较返回值；其他场景中，状态、异常、交互与终止性都可能重要。
定义与比较程序行为的方法
操作语义用转移规则或完整求值规则描述执行。指称语义组合式地赋予数学含义：复合表达式的含义由各部分的含义构成。所选数学域可以表示部分性或副作用；当持续交互也能被观察时，用一个不加区分的值表示所有不终止行为，未必足够。
对于 x := x+1，操作规则更新当前存储；指称描述则可以赋予一个把输入存储映射到更新后存储的函数。它们描述命令做什么。公理语义通过断言描述保证：在数学整数上，{x=4} x:=x+1 {x=5} 记录了这一变换的一项性质。在部分正确性的 Hoare 逻辑中，{P} C {Q} 表示：从满足 P 的状态开始，C 的任何终止执行都以满足 Q 结束。完全正确性还要求终止。完全正确性的最弱前置条件必须保证终止；最弱宽松前置条件处理的则是部分正确性。对于整数命令 x:=x+1 与预期结果 x≥0，最弱前置条件是 x≥−1：把赋值表达式代入预期条件，得到 x+1≥0。循环还需要不变式，完全正确性还需要终止论证。这个计算显示了后置条件怎样引导我们反向推理程序。
上下文等价追问：允许的周围程序，能否通过选定的观察区分两个组件？在适当的、可靠的组合式模型中，指称相等蕴涵上下文等价；反方向则是额外性质，称为完全抽象，并不是每个指称模型都自动满足。双模拟提供另一种方法，比较两个系统能否匹配彼此的步骤。
分离逻辑扩展了关于内存的断言式推理。分离合取描述堆中互不重叠的部分，框架规则则在满足附带条件时，使局部证明能够携带未触及的资源。例如，如果命令只修改地址 p 的单元，关于该单元的证明就可以携带一个关于独立地址 q 的断言。不相交条件排除了二者互为别名的情况。框架规则明确了为什么改变一部分内存，能够保持关于另一部分的断言。
递归解释了为什么指称模型需要超出普通全函数的结构。一种方法从未定义的近似开始，反复展开递归定义。对于阶乘，第一次展开可以定义零处的结果，后续展开再定义一处的结果，以此类推。在适当的有序域中，这些逐步增加信息的近似的极限，给出最小不动点。域及连续性条件为构造提供根据；仅有不动点方程，不一定能选定预期含义。
类型系统与可靠性
类型系统给表达式分类，并在执行前拒绝某些组合。对许多小型演算，可靠性通过两项性质证明：进展性意味着封闭的良类型表达式要么是值，要么能迈出一步；保持性意味着一步执行保持类型。两者共同排除指定的卡住状态，却不自动排除不终止、被处理的异常，或不符合用户目的的结果。
类型推断重建缺失的类型信息。Hindley–Milner 推断把合一与 let 多态结合起来，在其适用框架中提供主类型。合一求解未知类型之间的等式：如果 + 只表示整数加法，λx. x+1 就要求参数与结果都是整数。相比之下，由 let 绑定的恒等函数可以具有一般类型 A → A，在应用于整数和布尔值时分别实例化。主类型记录最一般的类型，由它得到允许的各个实例。它在实践中常常有效，但一般最坏情形并不是多项式时间；反复的多态使用可能产生极大的类型。Cornell 的说明区分了实际表现与这一复杂度界。更丰富的特性可能需要注解或不同算法。
参数性在指定语义下约束多态行为。在纯、全定义且满足参数性的演算中，类型为 ∀A. A → A 的封闭项必须返回其参数。加入一般递归后，它可能发散；加入副作用后，它可能执行其他可观察工作。有用的“免费定理”会说明前提，而不是把所有语言中的泛型函数都当成构造性证明。
操作技术：大步与小步
小步语义逐次记录转移 e → e′，大步语义记录一次完成的求值 e ⇓ v。普通的归纳式大步规则，可能对发散和卡住的项都不给出结果；要区分两者，需要额外判断或另一种表述。小步轨迹更容易描述无限执行与交错执行。
即使没有可变状态，求值顺序也会产生后果。记号 λx. e 表示参数为 x、函数体为 e 的函数；应用它时，按照求值规则使用参数替换。令 Ω 表示发散的计算。在 (λx. 1) Ω 中，按值调用先求参数，因此发散；按名调用因为没有使用参数，可以返回 1。按需调用还会共享已经求出的结果。求值上下文规定下一次归约可以发生在哪里，是明确这些选择的紧凑方法。
增加语言特性时，应追问哪些规则改变了、哪些既有定理需要重新检查。引用、异常与并发，可能使仅对纯且终止的核心证明过的论证失效。必须把新增特性写进规则并检查论证，才能对扩展后的语言继续主张原来的保证。
学习这个主题会改变什么
实际收获是一套比较行为的语言。重构前，说明哪些观察必须保持不变。依赖类型错误来排除缺陷前，识别类型系统真正强制的性质。把编译器优化当成代数变换前，先考虑算术与副作用。
一个有用的练习是定义极小的表达式语言，编写求值器和几条推理规则，再增加异常等一种特性。比较新规则与旧的进展性或等价性论证。这样，不必先构建完整编译器或掌握证明助手，就能把形式记号连接到具体设计选择。
资源
书籍与文本
Pierce 的 Types and Programming Languages（TAPL，2002）通过形式规则、例子与证明，展开带类型 lambda 演算、子类型、递归类型与多态。它需要归纳法和数学记号基础。可以先做小型类型推导与保持性论证，再进入更丰富的系统。Advanced Topics in Types and Programming Languages（ATTAPL，2005）收录进一步讨论，包括依赖类型、副作用与带类型的底层编程。
Harper 的 Practical Foundations for Programming Languages（PFPL，第 2 版，Cambridge，2016，网上有免费草稿）覆盖面比 TAPL 更广——包括命令式特性、并发，以及对高级类型论更完整的处理——但写作更密集。PFPL 围绕 “abstract binding trees” 组织，这是一种用于推理带绑定语法的形式系统，比 TAPL 中的呈现方式更一般。愿意投入阅读这种密集表达的读者，会获得更完整、更当代的领域图景。
Winskel 的 The Formal Semantics of Programming Languages（1993）讨论操作语义、域论与指称语义。关心怎样赋予程序含义、怎样连接不同的行为描述时，可以使用这本书。学习定义时，可配合小型求值器与存储变换例子。
Friedman 和 Wand 的 Essentials of Programming Languages（EOPL，第 3 版，MIT Press，2008）通过实现进入材料：读者会为复杂度逐步上升的语言构建解释器，而类型系统和语义概念则在工作实现的语境中被引入。对于一开始觉得形式文本过于抽象的读者，EOPL 更容易进入，并且明确展示理论与实现之间的连接。对 TAPL 节奏感到吃力的读者，先读 EOPL 再读 TAPL 是一条有效路线。
Krishnamurthi 的 Programming Languages: Application and Interpretation（PLAI，在线免费；可选付费纸质版）是另一条实现优先路线，通过解释器和语言变体使语义思想具体化。它没有 TAPL 和 PFPL 那样深的数学深度，但对需要先构建语言、再舒服地证明语言性质的程序员来说，是最好的桥梁之一。
Reynolds 的 Theories of Programming Languages（1998）详细讨论语言语义与程序推理。若专门学习分离逻辑，可阅读他后来的 2002 年论文，不应把这一后续发展归入 1998 年的书。
对于 基于证明助手的编程语言理论，Pierce 等人的 Software Foundations 系列（softwarefoundations.cis.upenn.edu 免费）是必要资源。第一卷 Logical Foundations 在教授逻辑和证明的同时教授 Coq；第二卷 Programming Language Foundations 在 Coq 中形式化操作语义、类型系统和 Hoare logic。这个系列是机制化形式下 PLT 的标准处理，也越来越成为任何计划做形式验证工作的人必须阅读的内容。
对于 进程演算和并发语言，Milner 的 Communicating and Mobile Systems: the Pi-Calculus（Cambridge，1999）是 pi-calculus 的主要来源；Sangiorgi 和 Walker 的 The Pi-Calculus: A Theory of Mobile Processes（Cambridge，2001）则是综合参考。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Pierce，Types and Programming Languages（TAPL） | 经典入口；类型系统 | 入门 |
| Pierce 编，Advanced Topics in Types and Programming Languages（ATTAPL） | TAPL 的延伸 | 深入 |
| Harper，Practical Foundations for Programming Languages（PFPL，草稿免费） | 更广泛的综合替代文本 | 深入 |
| Winskel，The Formal Semantics of Programming Languages | 操作语义与指称语义 | 深入 |
| Friedman & Wand，Essentials of Programming Languages（EOPL） | 实现优先的易进入入口 | 实践 |
| Krishnamurthi，PLAI（免费；可选付费纸质版） | 实现优先的 PL 概念 | 入门 |
| Reynolds，Theories of Programming Languages | 指称语义 + 公理语义深入处理 | 深入 |
| Pierce 等，Software Foundations Vols. 1–2（免费） | Coq 中的机制化 PLT | 实践 |
| Milner，Communicating and Mobile Systems | Pi-calculus 一手来源 | 深入 |
课程与讲座
Penn CIS 500（Software Foundations，Benjamin Pierce，免费材料）是 TAPL 最初对应的课程。完整讲义 slides 和补充材料都可以免费获取。Pierce 的教学把形式材料与编程练习结合起来，而课程结构也显示了教材背后的教学方法。
Carnegie Mellon 15-312（Principles of Programming Languages，Robert Harper，免费材料）使用 PFPL，是 Harper 的主要教学载体。他的讲义以其一贯的直接风格展开材料，针对具体主题，可以与 PFPL 一起读，或替代 PFPL 阅读。
Oregon Programming Languages Summer School（OPLSS） 每年在 Eugene 举办，并在 YouTube 免费提供讲座存档。OPLSS 吸引一线研究者，讲座系列覆盖从入门 PLT 到研究前沿的主题。优先推荐的具体系列：Frank Pfenning 关于证明论和类型论；Andrew Pitts 关于 nominal techniques；Paul-André Melliès 关于线性逻辑和 game semantics。
Software Foundations 的 Coq 练习，可在 softwarefoundations.cis.upenn.edu 获取，构成一门自定节奏课程，在发展 PLT 内容的同时发展机制化证明能力。完成第二卷会同时获得 PLT 知识和 Coq 能力。
| 课程 | 平台 | 类型 |
|---|---|---|
| Penn CIS 500 Software Foundations（Pierce，免费） | Penn 课程网站 | 入门 |
| CMU 15-312 Principles of PL（Harper，免费） | CMU 课程网站 | 深入 |
| OPLSS 讲座（免费） | YouTube / OPLSS 网站 | 参考 |
| Software Foundations 的 Coq 练习（免费） | softwarefoundations.cis.upenn.edu | 实践 |
实践、工具与当前来源
可以为同一个表达式写出小步归约序列与类型推导，再改变一条语言规则，识别哪些推导仍然成立。这把推理规则连接到它们描述的行为。
PLT Redex 是基于 Racket 的操作语义定义与测试环境。其配套书 Semantics Engineering with PLT Redex 由 Felleisen、Findler 与 Flatt 编写。可以实现小型表达式语言，查看归约轨迹，并用生成的测试寻找所提性质的反例。对模型的测试可以补充其一般性质的证明。
Andrej Bauer 和 Matija Pretnar 的 Programming Languages Zoo（免费）是一组微型语言集合，展示解析、解释器、编译器、静态和动态类型、子类型、多态、惰性求值、异常和抽象机。它尤其适合读者已经学过概念之后，用来并排查看紧凑实现。
Rocq/Coq、Lean 或 Agda 可以检查形式化的类型可靠性论证。应选择与工具及语言版本匹配的教程。Software Foundations 提供进展性、保持性与 Hoare 逻辑的系统练习；证明状态会显示缺失的情况与假设。
POPLmark Challenge（poplmark.org）在 2005 年为 PLT 元理论提出了一组基准证明；各种证明助手中的解法都可以免费获得，是机制化 PLT 的 worked examples。
| 资源 | 平台 | 类型 |
|---|---|---|
| PLT Redex（免费） | Racket / racket-lang.org | 实践 |
| Programming Languages Zoo（免费） | plzoo.andrej.com | 实践 |
| Software Foundations in Coq（免费） | softwarefoundations.cis.upenn.edu | 实践 |
| POPLmark challenge solutions（免费） | poplmark.org | 实践 |
| Lean 4 / Mathlib PLT formalizations（免费） | leanprover-community.github.io | 参考 |
陷阱
| 陷阱 | 为什么会误导 | 更好的做法 |
|---|---|---|
| 把实现行为等同于规格 | 某个实现可能从允许的行为中作选择，也可能有缺陷。 | 区分语言规则与对具体实现的观察。 |
| 把“良类型”读成“正确” | 可靠性排除指定失败，而不是所有不想要的结果。 | 说明卡住状态、副作用与终止假设。 |
| 认为代数改写普遍有效 | 求值顺序、溢出和副作用可能改变观察。 | 证明优化前，先说明语义模型。 |
| 认为指称相等刻画所有等价 | 完全抽象是模型的额外性质。 | 指定上下文观察，以及已经证明了哪个方向。 |
| 认为可判定推断总是很快 | 会终止的算法也可能具有很高的最坏成本。 | 区分推断、检查与推断类型的大小。 |
| 把纯语言定理搬进有副作用的语言 | 新增操作可能违反定理前提。 | 语言或观察模型改变时，重新检查论证。 |