English
Type theory studies systems for classifying terms and the rules for constructing and using them. A type can describe a kind of value, such as an integer, or a more precise requirement, such as a list containing exactly three elements. A typing judgment records that a term has a type under specified assumptions.
The subject connects programming language design to mathematical proof. In suitable systems, constructing a term of a type is also constructing evidence for a proposition. This lets a compiler reject an invalid combination of values, or a proof assistant check a mathematical argument, using related machinery. Section 3.4 explains the programming-language perspective; this section develops the connection to propositions and specifications.
Begin with functions, products, sum types, and induction. A product holds both components; a sum holds one of several tagged alternatives. These ordinary data structures provide concrete examples before dependent types, universes, or foundations of mathematics become necessary.
From Paradox Resolution to the Foundations of Mathematics
Types first entered foundational work as restrictions on forming expressions. Russell’s response to the paradoxes used a hierarchy to block problematic self-application and unrestricted comprehension. These early systems were more elaborate than the simple division of programming values into integers and strings. Their purpose was to control which mathematical constructions were legitimate.
Church’s simple theory of types combined typed functions with logic. Curry’s observations and Howard’s later account connected particular typed calculi to proof systems: function formation and application correspond to implication introduction and elimination. This was a correspondence between rules and derivations, not just a resemblance between the words “proof” and “program.” Wadler’s historical account explains how several lines of work contributed.
Martin-Löf’s work in the 1970s developed dependent type theory as a constructive foundation. Coquand and Huet’s Calculus of Constructions and subsequent developments supported the Coq proof assistant, now named Rocq. Agda and Lean also use dependent types, but proof assistants do not all share this foundation: HOL-family systems use forms of higher-order logic. A proof assistant is a way of checking proofs; dependent type theory is one possible logical basis.
Homotopy type theory later connected identity types with paths and their higher-dimensional structure. The univalence principle relates equality of types in a universe to equivalence of those types. It does not say that all types are equal. This work broadens the mathematical uses of types; ordinary indexed data structures can be understood without mastering these foundations first.
The Propositions-as-Types Correspondence and Its Depth
Read a proposition by asking what evidence would establish it. Evidence for “A and B” must contain both parts. Evidence for “A or B” must identify a side and provide its evidence. Evidence for “if A, then B” must explain how evidence for A yields evidence for B. These requirements lead directly to products, tagged sums, and functions.
What Curry-Howard Actually Says
In a basic constructive correspondence, propositions are types and proofs are terms. Conjunction corresponds to a product A × B, disjunction to a tagged sum A + B, and implication to a function type A → B. The empty type represents falsehood: it has no constructor. A proof of negation ¬A is a function from evidence for A to the empty type.
For example, the function swap(p) = (p.second, p.first) has type A × B → B × A. Its implementation also proves that A ∧ B implies B ∧ A. Applying a proof of A → B to a proof of A corresponds to modus ponens. Reducing first((a,b)) to a removes a construction immediately followed by its elimination; the same operation simplifies both a program and its associated proof.
Three tasks must be distinguished. Type checking verifies a supplied term against a proposed type. Type inference reconstructs omitted type information. Inhabitation asks whether any term of a type exists; under the correspondence, this is proof search. Checking a supplied proof may be decidable even when there is no general algorithm that decides whether a proposition has a proof.
The correspondence depends on the rules of the calculus. In a programming language with unrestricted recursion, loop() = loop() can be assigned many result types without producing a value. If such a term counted as a proof of the empty type, the logical interpretation would become inconsistent. Proof-oriented cores therefore control recursion and computation, or otherwise distinguish executable programs from logical evidence. A type annotation alone is not enough.
Dependent Types as a Specification Language
A dependent type may refer to a value. Let Vec A n describe sequences of elements of type A with length n. In schematic notation, concatenation has type append : Vec A m → Vec A n → Vec A (m+n). The result type records a relationship among the inputs and output, so an implementation returning a sequence of the wrong length cannot satisfy it.
The constructors explain how that information is maintained: the empty vector has length zero, and adding one element changes length n to n+1. Consequently, head : Vec A (n+1) → A needs no empty-input case. Alternatively, Fin n represents indices from zero through n−1, and get : Vec A n → Fin n → A requires an index valid for that particular length. The obligation to establish a valid index still exists; the type makes explicit where it must be discharged.
Dependent functions, written Πx:A. B(x), return a value whose type depends on the argument. Dependent pairs, written Σx:A. B(x), contain a value and evidence of a property of that value. A specification for sorting can return a list together with evidence that it is ordered and is a permutation of the input. Ordering alone permits returning the empty list every time. This example shows why a richer type helps only after the intended property has been chosen correctly.
Computation can settle some equalities automatically: closed arithmetic expressions such as 2+3 can reduce to 5. General facts about arbitrary inputs, such as commutativity of addition, require a proof. This distinguishes definitional equality, recognized through the system’s computation rules, from propositional equality, for which an explicit proof term may be needed. It explains why two mathematically equal lengths can still require a small lemma in a program.
Universe levels control statements about types themselves. They avoid unrestricted self-reference such as treating one universe as containing itself without restriction. The details matter when formalizing foundations or writing highly generic libraries; beginners can first use the universe structure provided by their tool. Dependent types do not imply that every practical inference problem is solved automatically: annotations, termination arguments, and proof obligations can still be substantial.
Constructivity and Its Consequences
Constructive reasoning keeps track of how evidence is obtained. To establish an existential claim in a dependent-pair formulation, supply a witness and its evidence. A proof that every input admits such an output can then describe a procedure for producing outputs. Whether the resulting procedure is efficient is a separate question: existence of a terminating computation does not establish a useful time bound.
Classical logic remains usable in proof assistants. It is incorrect to say that it has no computational interpretation: translations and control operators provide important connections. But adding classical existence principles need not provide an executable witness-selection algorithm. Lean’s account of axioms and computation distinguishes checked reasoning from definitions that depend on noncomputable choices. A logical existential proposition is also not always represented as a runtime pair; systems may erase proofs or restrict elimination from propositions into data.
The constructive dependent-pair form of choice illustrates the distinction. If h supplies a pair (y, evidence) for every x, define the choice function by taking the first component of h(x). The needed witnesses were already part of the premise. This is different from assuming a classical set-theoretic choice principle for arbitrary collections.
When reading a verified program, ask which computations terminate, which axioms are assumed, and which parts are erased or extracted. When reading a proof assistant’s success message, also check for admitted statements or unchecked external results. These questions locate the evidence; they do not diminish the value of checking the complete derivation.
What Studying This Changes
Types become a way to assign responsibilities. A plain integer index makes the caller and callee agree informally about bounds. A bounded index records the requirement at their interface. A sorting result with ordering and permutation evidence records two different obligations that tests may otherwise conflate.
For practice, first implement the pair-swapping proof, then a nonempty-list head operation, and finally length-preserving vector operations. Deliberately remove one condition from a specification and find an incorrect implementation that now passes. This teaches both what the type system guarantees and why writing the specification remains a design task.
Resources
Books and Texts
Pierce’s Types and Programming Languages (TAPL, 2002) develops the typed calculi needed to understand many programming-language uses of types. Use it for typing rules, evaluation, and soundness. Advanced Topics in Types and Programming Languages (ATTAPL, 2005) provides further treatments including dependent types. For a direct introduction to dependent programming, the programming-oriented books below provide more focused exercises.
Martin-Löf’s Intuitionistic Type Theory, based on the Padua lectures, is a primary source for constructive dependent type theory. It distinguishes judgments about types, terms, and their equalities, then organizes rules for constructing and using them. Its foundational style differs from a programming tutorial. It explains an influential family of foundations, not the basis of every proof assistant.
The Homotopy Type Theory Book (HoTT Book, 2013, free at homotopytypetheory.org) is the collaborative presentation of homotopy type theory produced by the IAS special year. It covers Martin-Löf type theory, homotopy-theoretic interpretation, the univalence axiom, and substantial developments in synthetic homotopy theory. It is mathematically demanding — assumes comfort with abstract algebra and some topology — but is a useful reference for the contemporary frontier of type theory. Reading the introduction and the first two chapters is accessible to readers with solid PLT background; the later chapters require more.
For guided proof exercises, choose among Software Foundations in Rocq/Coq, Programming Language Foundations in Agda (Wadler, Kokke, and Siek), and Theorem Proving in Lean 4 with Mathematics in Lean. The first two connect proof construction to programming-language metatheory; the Lean materials also support mathematical formalization. Matching the tool to a sustained exercise sequence is more useful initially than installing several environments.
Brady’s Type-Driven Development with Idris (2017) teaches dependent types through programming: write a specification as a type and use the remaining type obligations to guide implementation. Friedman and Christiansen’s The Little Typer develops related ideas through a dialogue and small examples. Choose the former for larger programming exercises or the latter for a gradual introduction to the core constructions.
Nordström, Petersson, and Smith’s Programming in Martin-Löf’s Type Theory (1990, free online) is the systematic textbook presentation of Martin-Löf type theory. It is less demanding than the original lecture notes and more systematic; a useful companion to the Padua notes for learners who want a structured presentation.
| Book | Role | Type |
|---|---|---|
| Type-theory chapters in Pierce, Types and Programming Languages (TAPL) | Entry to typed lambda calculi and Curry-Howard | Entry |
| Advanced type-system chapters in ATTAPL | Dependent types, effects, linear types | Depth |
| Martin-Löf, Intuitionistic Type Theory (Padua notes, free) | Primary source for dependent type theory | Depth |
| The HoTT Book (free) | Homotopy type theory; contemporary frontier | Depth |
| Type-theory track in Software Foundations Vols. 1-2 (free) | Mechanized PLT and type theory in Coq | Practice |
| Wadler et al., Programming Language Foundations in Agda (free) | Mechanized PLT in Agda | Practice |
| de Moura et al., Theorem Proving in Lean 4 (free) | Lean 4 tutorial | Practice |
| Avigad & Massot, Mathematics in Lean (free) | Mathematical formalization in Lean | Practice |
| Brady, Type-Driven Development with Idris (paid) | Dependent types as programming methodology | Depth |
| Friedman & Christiansen, The Little Typer (paid) | Gentle dependent-types intuition | Auxiliary |
| Nordström, Petersson & Smith, Programming in Martin-Löf’s Type Theory (free) | Systematic Martin-Löf type theory | Depth |
| Type-theoretic foundations in Harper, PFPL (draft free) | Broader PLT with type-theoretic grounding | Depth |
| Dependent-type verification in Chlipala, Certified Programming with Dependent Types (free) | Coq-based verified software development | Depth |
Courses and Lectures
OPLSS archives include lectures by Frank Pfenning on proof theory and logical frameworks, Robert Harper on type theory, and Stephanie Weirich on type inference. Select a series after checking its prerequisites, and use the accompanying definitions and examples to practice individual derivations.
CMU 15-317 Constructive Logic develops proofs, programs, and their correspondence; 15-312 Principles of Programming Languages connects typing and semantics to language design. Choose a specific archived offering so that the lecture sequence, instructor, and exercises can be identified together.
The Lean 4 community at leanprover-community.github.io maintains extensive tutorials, the Zulip chat, and structured learning paths for both programming and mathematical formalization. The community provides support for a research-oriented mathematical tool.
Agda community resources at agda.readthedocs.io and through the PLFA book provide structured learning paths. The Agda Zulip is also active.
| Course | Platform | Type |
|---|---|---|
| OPLSS lectures — Pfenning, Harper, Weirich (free) | YouTube / OPLSS site | Reference |
| CMU 15-317 Constructive Logic (Harper, free) | CMU course site | Entry |
| Type-theory sequence in CMU 15-312 Principles of PL (Harper, free) | CMU course site | Depth |
| Lean 4 community tutorials (free) | leanprover-community.github.io | Practice |
Practice, Tools, and Current Sources
Construct small proofs and inspect the resulting terms or proof states. When a step fails, identify whether the problem is an incorrect proposition, a missing assumption, an unresolved equality, or a limitation of automation. These are different obstacles and require different responses.
Lean 4 with mathlib supports mathematical formalization. Follow the setup instructions for the selected edition of Mathematics in Lean, then read source proofs of statements you already understand. Compare the informal argument with the lemmas and instances used by the checked proof.
Agda with PLFA provides a programming-oriented sequence. Follow PLFA’s version-specific installation instructions, then work through its inductive data types, functions, and proofs. Keeping the exercise version and library version aligned avoids confusing setup problems with type-theoretic ones.
Coq with Software Foundations: install through opam, work through Volume 2 (Programming Language Foundations). The PLT-specific content — operational semantics, type soundness, Hoare logic — is the most directly connected to §3.4.
Proof General (Emacs) or VSCoq (VS Code) provide interactive proof development interfaces where the proof state is visible after each tactic — essential for understanding what is happening during proof construction.
| Resource | Platform | Type |
|---|---|---|
| Lean 4 + mathlib (free) | elan / github.com/leanprover | Practice |
| Agda + PLFA (free) | agda.readthedocs.io | Practice |
| Coq + Software Foundations (free) | coq.inria.fr / softwarefoundations.cis.upenn.edu | Practice |
| Lean Zulip (free) | leanprover.zulipchat.com | Reference |
| mathlib4 source (free) | github.com/leanprover-community/mathlib4 | Reference |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Calling any typed program a proof | Unrestricted recursion can produce a term that never supplies evidence. | Identify the logical core and its treatment of termination. |
| Confusing checking with proof discovery | Verifying a supplied derivation differs from finding one. | Separate checking, inference, and inhabitation. |
| Expecting a rich type to repair a weak specification | “Sorted” alone permits an empty output for every input. | State all required relationships, including preservation of input elements. |
| Treating every existential as runtime data | Logical propositions and computational pairs can have different elimination and erasure rules. | Check the proof assistant’s representation and extraction rules. |
| Saying classical logic has no computational interpretation | Translations and control-based interpretations exist. | Distinguish logical admissibility from an executable witness-producing program. |
| Assuming every proof assistant uses dependent types | HOL-family foundations differ from dependent type theories. | Learn the particular system’s logic, axioms, and trusted checking mechanism. |
中文
类型论研究对项进行分类的系统，以及构造和使用这些项的规则。类型可以描述一类值，例如整数；也可以表达更精确的要求，例如恰好包含三个元素的列表。类型判断记录：在指定假设下，一个项具有某种类型。
这门学科把编程语言设计与数学证明联系起来。在适当的系统中，构造某个类型的项，也是在构造某个命题的证据。因此，编译器拒绝无效的值组合，与证明助手检查数学论证，可以使用相互关联的机制。§3.4 介绍编程语言的视角，这里进一步解释类型与命题、规约的联系。
从函数、积类型、和类型与归纳法开始。积类型同时保存各个分量；和类型保存若干带标记的备选情况之一。这些普通数据结构提供了具体例子，不必一开始就进入依赖类型、宇宙或数学基础。
从解决悖论到数学基础
类型最初进入基础研究，是为了限制表达式的构成。Russell 应对悖论的办法使用层级，阻止有问题的自我应用与不受限制的概括。这些早期系统比把程序值分成整数和字符串复杂得多，其目的是约束哪些数学构造是合法的。
Church 的简单类型论把带类型的函数与逻辑结合起来。Curry 的观察和 Howard 后来的论述，把特定的带类型演算连接到证明系统：构造函数与应用函数，分别对应蕴涵的引入与消去。这是规则和推导之间的对应，不只是“证明”与“程序”两个词的相似。Wadler 的历史论述解释了多条研究线索的贡献。
Martin-Löf 在二十世纪七十年代发展了作为构造性基础的依赖类型论。Coquand 与 Huet 的构造演算及其后续发展，支持了 Coq 证明助手；Coq 现名 Rocq。Agda 和 Lean 也使用依赖类型，但证明助手并不都采用这种基础：HOL 系列使用高阶逻辑的不同形式。证明助手是一种检查证明的工具，依赖类型论则是可选的逻辑基础之一。
后来的同伦类型论把恒等类型（identity type）连接到路径及其更高维结构。单价性原理把一个宇宙中类型的相等与这些类型之间的等价联系起来，并不是说所有类型都相等。这些工作扩展了类型的数学用途；理解普通的索引数据结构，并不需要先掌握这些基础研究。
命题即类型对应及其深度
理解一个命题，可以先问什么证据能建立它。“A 且 B”的证据必须包含两部分；“A 或 B”的证据必须指明哪一边成立，并提供那一边的证据；“如果 A，那么 B”的证据，必须说明怎样从 A 的证据得到 B 的证据。这些要求直接对应积、带标记的和，以及函数。
Curry-Howard 实际上说了什么
在基本的构造性对应中，命题是类型，证明是项。合取对应积类型 A × B，析取对应带标记的和类型 A + B，蕴涵对应函数类型 A → B。空类型表示假：它没有构造子。否定 ¬A 的证明，是一个把 A 的证据变成空类型的函数。
例如，函数 swap(p) = (p.second, p.first) 的类型是 A × B → B × A。它的实现也证明了 A ∧ B 蕴涵 B ∧ A。把 A → B 的证明应用于 A 的证明，对应肯定前件推理。把 first((a,b)) 化简为 a，消除了紧接构造之后的消去；同一操作同时简化了程序与相应证明。
这里需要区分三项任务。类型检查核验给定项是否具有指定类型；类型推断重建省略的类型信息；类型居留问题问某个类型是否存在任何项，在这一对应下就是证明搜索。检查给定证明可能是可判定的，即使不存在能够一般地判定某个命题是否有证明的算法。
这种对应依赖演算的规则。在允许不受限制递归的编程语言中，loop() = loop() 可以被赋予多种结果类型，却不产生值。如果把这样的项当成空类型的证明，逻辑解释就会变得不一致。因此，用于证明的核心系统需要控制递归与计算，或用其他方式区分可执行程序与逻辑证据。仅有类型注解并不够。
依赖类型作为规约语言
依赖类型可以引用一个值。令 Vec A n 表示由 A 类型元素构成、长度为 n 的序列。使用示意记号，拼接的类型是 append : Vec A m → Vec A n → Vec A (m+n)。结果类型记录输入与输出之间的关系，因此，返回错误长度序列的实现无法满足这个类型。
构造子说明了怎样维持这些信息：空向量长度为零，增加一个元素会把长度从 n 变为 n+1。因此，head : Vec A (n+1) → A 不需要处理空输入。另一种方式是让 Fin n 表示零到 n−1 的索引，则 get : Vec A n → Fin n → A 要求索引对这个特定长度有效。建立索引有效性的责任仍然存在；类型明确了必须在哪里完成它。
依赖函数写成 Πx:A. B(x)，返回值的类型依赖参数。依赖对写成 Σx:A. B(x)，包含一个值以及该值满足某个性质的证据。排序的规约可以要求返回列表，同时证明它有序，并且是输入的一个排列。只要求有序，就允许实现每次返回空列表。这个例子说明，先选对要表达的性质，更丰富的类型才能起作用。
计算能够自动解决一些相等关系：2+3 这样的封闭算术表达式可以化简为 5。对于任意输入成立的一般事实，例如加法交换律，则需要证明。这区分了通过系统计算规则识别的定义相等，以及可能需要显式证明项的命题相等。它也解释了为什么两个数学上相等的长度，在程序中仍可能需要一个小引理。
宇宙层级控制关于类型本身的陈述，避免不受限制的自我引用，例如毫无限制地让一个宇宙包含自身。形式化基础或编写高度泛化的库时，这些细节很重要；初学者可以先使用工具提供的宇宙结构。依赖类型不意味着实际推断问题都能自动解决：注解、终止论证和证明义务仍然可能需要不少工作。
构造性及其后果
构造性推理追踪证据是怎样获得的。用依赖对表达存在性时，需要给出见证及其证据。证明每个输入都存在这样的输出，就可以描述一个产生输出的过程。过程是否高效是另一回事：存在终止计算，并不建立有用的时间界。
证明助手仍然可以使用经典逻辑。说经典逻辑没有计算解释是不正确的：逻辑翻译与控制算子提供了重要联系。不过，加入经典存在性原理，并不一定能得到可执行的见证选择算法。Lean 关于公理与计算的说明区分了经过检查的推理，以及依赖不可计算选择的定义。逻辑存在命题也不一定表示成运行时的一对数据；系统可能擦除证明，或限制从命题到数据的消去。
选择原理的构造性依赖对形式可以说明这个区别。如果 h 对每个 x 都提供一对 (y, evidence)，那么取出 h(x) 的第一分量，就能定义选择函数。所需见证已经包含在前提中。这与对任意集合族假设经典集合论的选择原理，是不同的事情。
阅读经过验证的程序时，应问哪些计算会终止、假设了哪些公理、哪些部分会被擦除或提取。阅读证明助手的成功信息时，也应检查是否存在直接承认的命题或未经检查的外部结果。这些问题帮助定位证据，并不削弱检查完整推导的价值。
学习这个主题会改变什么
类型成为分配责任的一种方式。普通整数索引要求调用者与被调用者对边界作非形式约定；有界索引把要求写在二者的接口上。附带有序性与排列证据的排序结果，则记录了测试中容易混在一起的两项义务。
可以先实现交换一对分量的证明，再实现非空列表的取首项操作，最后实现保持长度关系的向量操作。刻意从规约中删去一个条件，寻找现在能够通过的错误实现。这样既能理解类型系统的保证，也能理解为什么编写规约仍然是一项设计工作。
资源
书籍与文本
Pierce 的 Types and Programming Languages（TAPL，2002）发展了理解编程语言类型用途所需的带类型演算，可用于学习类型规则、求值与可靠性。Advanced Topics in Types and Programming Languages（ATTAPL，2005）提供包括依赖类型在内的进一步讨论。如果希望直接学习依赖类型编程，下面面向编程的书提供了更集中的练习。
Martin-Löf 基于 Padua 讲座的 Intuitionistic Type Theory 是构造性依赖类型论的一手材料。它区分关于类型、项及其相等的判断，再组织构造与使用它们的规则。它的基础研究写法不同于编程教程，解释的是一族有影响的基础，而不是所有证明助手的基础。
Homotopy Type Theory Book（HoTT Book，2013，可在 homotopytypetheory.org 免费获取）是 IAS 特别年度产生的同伦类型论协作呈现。它覆盖 Martin-Löf 类型论、同伦论解释、单价公理，以及 synthetic homotopy theory 中的大量发展。它数学要求较高——预设读者熟悉抽象代数和部分拓扑学——但它是当代类型论前沿的可用参考。对拥有扎实 PLT 背景的读者而言，导论和前两章可以进入；后续章节要求更高。
练习证明构造时，可以选择 Rocq/Coq 中的 Software Foundations、Wadler、Kokke 与 Siek 的 Programming Language Foundations in Agda，或 Theorem Proving in Lean 4 配合 Mathematics in Lean。前两者把证明构造连接到编程语言元理论，Lean 材料也支持数学形式化。起初，围绕一套连续练习选择匹配工具，比同时安装多个环境更有用。
Brady 的 Type-Driven Development with Idris（2017）通过编程教授依赖类型：把规约写成类型，用剩余的类型义务引导实现。Friedman 与 Christiansen 的 The Little Typer 通过对话和小例子发展相关概念。希望练习较完整的程序，可以选择前者；希望逐步学习核心构造，可以选择后者。
Nordström、Petersson 和 Smith 的 Programming in Martin-Löf’s Type Theory（1990，网上免费）是 Martin-Löf 类型论的系统教材式呈现。它比原始讲义要求更低，也更系统；对于想获得结构化呈现的学习者，它是 Padua 讲义的合适配套。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Pierce，Types and Programming Languages（TAPL）中的类型论章节 | 类型化 λ 演算与 Curry-Howard 的入口 | 入门 |
| ATTAPL 中的高级类型系统章节 | 依赖类型、效应、线性类型 | 深入 |
| Martin-Löf，Intuitionistic Type Theory（Padua notes，免费） | 依赖类型论一手来源 | 深入 |
| The HoTT Book（免费） | 同伦类型论；当代前沿 | 深入 |
| Software Foundations Vols. 1-2（免费）中的类型论路线 | Coq 中的机制化 PLT 和类型论 | 实践 |
| Wadler 等，Programming Language Foundations in Agda（免费） | Agda 中的机制化 PLT | 实践 |
| de Moura 等，Theorem Proving in Lean 4（免费） | Lean 4 教程 | 实践 |
| Avigad & Massot，Mathematics in Lean（免费） | Lean 中的数学形式化 | 实践 |
| Brady，Type-Driven Development with Idris（付费） | 依赖类型作为编程方法论 | 深入 |
| Friedman & Christiansen，The Little Typer（付费） | 温和的依赖类型直觉入口 | 辅助 |
| Nordström、Petersson & Smith，Programming in Martin-Löf’s Type Theory（免费） | 系统化 Martin-Löf 类型论 | 深入 |
| Harper，PFPL 中的类型论基础（草稿免费） | 具有类型论基础的更广泛 PLT | 深入 |
| Chlipala，Certified Programming with Dependent Types（免费）中的依赖类型验证 | 基于 Coq 的已验证软件开发 | 深入 |
课程与讲座
OPLSS 存档包含 Frank Pfenning 关于证明论和逻辑框架、Robert Harper 关于类型论，以及 Stephanie Weirich 关于类型推断的讲座。检查先修要求后选择一个系列，配合其中的定义和例子练习具体推导。
CMU 15-317 Constructive Logic 讨论证明、程序及其对应；15-312 Principles of Programming Languages 把类型与语义连接到语言设计。选择一个具体学期的存档，使讲课顺序、教师与练习能够对应起来。
Lean 4 community 位于 leanprover-community.github.io，维护大量教程、Zulip 聊天和面向编程与数学形式化的结构化学习路径。对于一个偏研究的数学工具而言，这个共同体提供交流支持。
Agda community resources 位于 agda.readthedocs.io，并通过 PLFA 一书提供结构化学习路径。Agda Zulip 也很活跃。
| 课程 | 平台 | 类型 |
|---|---|---|
| OPLSS 讲座——Pfenning、Harper、Weirich（免费） | YouTube / OPLSS 网站 | 参考 |
| CMU 15-317 Constructive Logic（Harper，免费） | CMU 课程网站 | 入门 |
| CMU 15-312 Principles of PL 中的类型论序列（Harper，免费） | CMU 课程网站 | 深入 |
| Lean 4 community tutorials（免费） | leanprover-community.github.io | 实践 |
实践、工具与当前来源
构造小型证明，并检查产生的项或证明状态。步骤失败时，识别问题来自命题不正确、缺少假设、未解决的相等关系，还是自动化能力的限制。这些障碍不同，处理方式也不同。
Lean 4 与 mathlib 支持数学形式化。按照选定版本 Mathematics in Lean 的配置说明开始，再阅读自己已经理解的命题的源码证明，比较非形式论证与检查后的证明使用了哪些引理和实例。
Agda 与 PLFA 提供面向编程的学习顺序。按照 PLFA 针对相应版本的安装说明开始，再学习归纳数据类型、函数与证明。使练习版本与库版本一致，可以避免把环境配置问题误当成类型论问题。
Coq 搭配 Software Foundations：通过 opam 安装，完成第二卷 Programming Language Foundations。其中 PLT 专属内容——操作语义、类型可靠性、Hoare logic——与 §3.4 最直接相关。
Proof General（Emacs）或 VSCoq（VS Code）提供交互式证明开发界面，能够在每一步 tactic 后显示证明状态——这对于理解证明构造中发生了什么是必要的。
| 资源 | 平台 | 类型 |
|---|---|---|
| Lean 4 + mathlib（免费） | elan / github.com/leanprover | 实践 |
| Agda + PLFA（免费） | agda.readthedocs.io | 实践 |
| Coq + Software Foundations（免费） | coq.inria.fr / softwarefoundations.cis.upenn.edu | 实践 |
| Lean Zulip（免费） | leanprover.zulipchat.com | 参考 |
| mathlib4 source（免费） | github.com/leanprover-community/mathlib4 | 参考 |
陷阱
| 陷阱 | 为什么会误导 | 更好的做法 |
|---|---|---|
| 把任意带类型程序称为证明 | 不受限制的递归可能永远不能提供证据。 | 识别逻辑核心及其对终止性的处理。 |
| 混淆检查与发现证明 | 核验给定推导与找到推导，是不同任务。 | 区分检查、推断与类型居留问题。 |
| 期望丰富类型弥补薄弱规约 | 仅要求“有序”，允许对每个输入都返回空列表。 | 写出全部关系要求，包括保留输入元素。 |
| 把每个存在命题都当成运行时数据 | 逻辑命题与计算性数据对可能采用不同消去、擦除规则。 | 检查证明助手的表示与提取规则。 |
| 说经典逻辑没有计算解释 | 存在逻辑翻译与基于控制操作的解释。 | 区分逻辑上的可用性与可执行的见证生成程序。 |
| 认为所有证明助手都用依赖类型 | HOL 系列的基础不同于依赖类型论。 | 学习具体系统的逻辑、公理与可信检查机制。 |