PL-Graph

graph TD

    %% ===== 基础逻辑 =====
    LogicInCS["Logic in
Computer Science
(Huth & Ryan)"]

    %% ===== 核心 PL / 类型系统 =====
    TAPL["Types and
Programming
Languages"]
    PFPL["Practical
Foundations for
Programming Languages"]

    %% ===== 语义学分支 =====
    SemanticsApp["Semantics with
Applications"]
    Winskel["Formal Semantics
(Winskel)"]
    CatProg["Category Theory
for Programmers"]

    %% ===== 构造逻辑 / 类型论 =====
    TTFP["Type Theory and
Formal Proof"]
    ProofsTypes["Proofs and
Types"]
    MLTTBook["Programming in
Martin-Löf Type
Theory"]

    %% ===== Coq / 形式化验证 =====
    SF["Software
Foundations"]
    CPDT["Certified
Programming with
Dependent Types"]
    Bertot["Interactive
Theorem Proving
(Bertot & Castéran)"]

    %% ===== HoTT =====
    HoTT["Homotopy Type
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;