PL-Graph

graph TD %% ===== 基础逻辑 ===== LogicInCS["Logic in<br/>Computer Science<br/>(Huth & Ryan)"] %% ===== 核心 PL / 类型系统 ===== TAPL["Types and<br/>Programming<br/>Languages"] PFPL["Practical<br/>Foundations for<br/>Programming Languages"] %% ===== 语义学分支 ===== SemanticsApp["Semantics with<br/>Applications"] Winskel["Formal Semantics<br/>(Winskel)"] CatProg["Category Theory<br/>for Programmers"] %% ===== 构造逻辑 / 类型论 ===== TTFP["Type Theory and<br/>Formal Proof"] ProofsTypes["Proofs and<br/>Types"] MLTTBook["Programming in<br/>Martin-Löf Type<br/>Theory"] %% ===== Coq / 形式化验证 ===== SF["Software<br/>Foundations"] CPDT["Certified<br/>Programming with<br/>Dependent Types"] Bertot["Interactive<br/>Theorem Proving<br/>(Bertot & Castéran)"] %% ===== HoTT ===== HoTT["Homotopy Type<br/>Theory (HoTT Book)"] %% ---------- 边：前置依赖 ---------- %% 基础 → 核心 PL LogicInCS --> TAPL %% TAPL → 更高阶 PL 理论 TAPL --> PFPL %% TAPL → 语义学 TAPL --> SemanticsApp SemanticsApp --> Winskel LogicInCS --> CatProg CatProg --> Winskel %% 基础 → 构造逻辑 / 类型论 LogicInCS --> TTFP TAPL --> TTFP LogicInCS --> ProofsTypes ProofsTypes --> MLTTBook TTFP --> MLTTBook %% 类型论 → Coq / 形式化验证 TTFP --> SF MLTTBook --> SF SF --> CPDT SF --> Bertot CPDT --> Bertot %% 类型论 / 范畴论 → HoTT MLTTBook --> HoTT CPDT --> HoTT CatProg --> HoTT %% ===== 推荐主线路径高亮 ===== %% LogicInCS → TAPL → TTFP → MLTTBook → SF → CPDT → HoTT classDef mainNode fill:#d0e8ff,stroke:#2b6cb0,stroke-width:2px; class LogicInCS,TAPL,TTFP,MLTTBook,SF,CPDT,HoTT mainNode;