09 · 文献与资源

说明：标注 [R] 的条目来自 etiamz/interaction-net-resources（BSD-3-Clause），链接已核对；其余为官方项目/文档。 引用时以原文为准；本文只做索引，不替代阅读。

9.1 入门与总览

• [R] Lafont, Yves. Interaction Nets. POPL 1989. https://dl.acm.org/doi/pdf/10.1145/96709.96718
• [R] Gay, Simon J. Interaction Nets. Diploma thesis, 1991. https://www.dcs.gla.ac.uk/~simon/publications/diploma.pdf
• [R] Wikipedia. Interaction nets. https://en.wikipedia.org/wiki/Interaction_nets
• [R] 资源总表（持续更新）. https://github.com/etiamz/interaction-net-resources
• [R] 精简版资源表. https://github.com/marvinborner/interaction-net-resources

9.2 交互组合子与通用性

• [R] Lafont, Yves. Interaction Combinators. Information and Computation 137(1), 1997. https://www.sciencedirect.com/science/article/pii/S0890540197926432
• [R] Mackie, Ian, and Jorge Sousa Pinto. Encoding linear logic with interaction combinators. 2002.
• [R] Fernández, Maribel. Type assignment and termination of interaction nets. 1998.

9.3 最优归约 / λ 编码

• [R] Lamping, John. An algorithm for optimal lambda calculus reduction. POPL 1989. https://dl.acm.org/doi/pdf/10.1145/96709.96711
• [R] Gonthier, Georges, Martín Abadi, and Jean-Jacques Lévy. The geometry of optimal lambda reduction. POPL 1992. https://dl.acm.org/doi/pdf/10.1145/143165.143172
• [R] Asperti, Andrea, and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1998.
• [R] Asperti, Andrea, and Cosimo Laneve. Interaction Systems I: The theory of optimal reductions. 1994. https://inria.hal.science/inria-00076988/document
• [R] Asperti, Andrea, and Cosimo Laneve. Interaction Systems II: The practice of optimal reductions. 1996.
• [R] Lawall, Julia L., and Harry G. Mairson. Optimality and inefficiency: what isn't a cost model of the lambda calculus? 1996. https://dl.acm.org/doi/pdf/10.1145/232629.232639
• [R] Asperti, Andrea. P = NP, up to sharing. 1997.
• [R] Mackie, Ian. YALE: Yet another lambda evaluator based on interaction nets. 1998. https://dl.acm.org/doi/pdf/10.1145/289423.289434
• [R] Lippi, Sylvain. Encoding left reduction in the λ-calculus with interaction nets. 2002.
• [R] Sinot, François-Régis. Call-by-name and call-by-value as token-passing interaction nets. 2005.

9.4 并发、multiport 与 π 演算

• [R] Mazza, Damiano. Interaction Nets: Semantics and Concurrent Extensions. PhD thesis, 2006. https://www.lipn.univ-paris13.fr/~mazza/papers/Thesis.pdf
• [R] Mazza, Damiano. Interaction Nets and Concurrency (AILA 2005 abstract). https://people.dm.unipi.it/aila2005/abstracts/mazza.pdf
• [R] Alexiev, Vladimir. PhD thesis on multiport interaction nets, 1999.
• [R] Khalil, Lionel. PhD thesis on multiport interaction nets / amb, 2003.
• [R] Dal Lago, Ugo, Ryo Tanaka, and Akira Yoshimizu. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. LICS 2017. https://ieeexplore.ieee.org/document/8005112/
• [R] Aschieri, Federico, and Francesco A. Genco. Par means parallel: multiplicative linear logic proofs as concurrent functional programs. POPL 2019. https://dl.acm.org/doi/10.1145/3371086
• [R] Mackie, Ian. Compiling process networks to interaction nets. 2016. https://arxiv.org/pdf/1609.03640
• [R] Fernández, Maribel, and Lionel Khalil. Interaction Nets with McCarthy's Amb. 2003.

9.5 实现与工程

• [R] Asperti, Andrea, et al. BOHM 1.1 (Bologna Optimal Higher-Order Machine). https://github.com/asperti/BOHM1.1
• [R] PECLR — parallel environment for optimal λ reduction. https://github.com/pis147879/PELCR
• [R] Optiscope — Lévy-optimal λ reducer with a C backdoor. https://github.com/etiamz/optiscope
• [R] Sato, Shinya. Design and implementation of a low-level language for interaction nets. PhD thesis, 2015. https://sussex.figshare.com/articles/thesis/Design_and_implementation_of_a_low-level_language_for_interaction_nets/23417312/1
• [R] Hassan, Abubakar, Ian Mackie, and Shinya Sato. An implementation model for interaction nets. 2015. https://arxiv.org/pdf/1505.07164
• [R] Mackie, Ian, and Shinya Sato. In-place graph rewriting with interaction nets. 2016. https://arxiv.org/pdf/1609.03641
• [R] Mackie, Ian, and Shinya Sato. Parallel evaluation of interaction nets: case studies and experiments. 2016. https://eceasst.org/index.php/eceasst/article/download/2205/2376/2387
• [R] Inpla — multi-threaded parallel interpreter of interaction nets. https://github.com/inpla/inpla
• [R] ingpu — experimental GPU evaluator. https://github.com/euschn/ingpu
• [R] Jiresch, Eugen. Towards a GPU-based implementation of interaction nets. 2014. https://arxiv.org/pdf/1404.0076
• [R] Linr — lightweight parallel computation server. http://cl-informatik.uibk.ac.at/users/sgimenez/lin/
• [R] GoI Visualizer — dynamic GoI abstract machine simulation. https://koko-m.github.io/GoI-Visualiser/
• [R] Huber, Nikolaus, and Wang Yi. An Encoding of Interaction Nets in OCaml. 2025. https://arxiv.org/pdf/2503.20463
• [R] Borner, Marvin. Optimal Interaction With the Real World. Bachelor's thesis, 2025. https://raw.githubusercontent.com/marvinborner/optimal-effects/refs/heads/bachelor/thesis.pdf

9.6 HVM / Bend / Vine 生态

• HVM2 — massively parallel Interaction Combinator evaluator. https://github.com/HigherOrderCO/HVM2
• HVM2 论文 — Taelin, Victor. HVM2: A Parallel Evaluator for Interaction Combinators. 2024. https://raw.githubusercontent.com/HigherOrderCO/HVM/main/paper/HVM2.pdf
• HVM3 — Interaction Calculus 实现（Haskell + C），IC.md / HVM.md / INTERS.md. https://github.com/HigherOrderCO/HVM3
• HVM4 — 单文件 C 实现，最新交互表/内存文档. https://github.com/HigherOrderCO/HVM4
• Bend — 高层语言 → HVM；2026 强调 LAWS.bend 与证明. https://github.com/HigherOrderCO/Bend https://bend-lang.com
• Vine / Ivy / IVM — 基于交互网的语言 + 低层 IC 语言 + 运行时. https://github.com/VineLang/vine https://vine.dev/docs/
• Interaction Calculus — 参考实现（C/Haskell）+ 规范. https://github.com/VictorTaelin/Interaction-Calculus

9.7 类型、线性逻辑与 session

• Girard, Jean-Yves. Linear Logic. 1987.
• Honda, Kohei. Types for Dyadic Interaction. CONCUR 1993.（session types 起源）
• Caires, Luís, and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. CONCUR 2010.
• Wadler, Philip. Propositions as Sessions. ICFP 2012.
• Danos, Vincent, and Laurent Regnier. The structure of multiplicatives. 1989.（proof net 正确性判据）
• Abramsky, Samson. Computational Interpretations of Linear Logic. 1993.（GoI）

9.8 Agent / 工作流 / 分布式基础设施

这些不是交互网文献，而是 Ainet 要对话/借鉴的系统。

• Temporal — durable execution, event history, activities. https://docs.temporal.io
• DBOS — durable workflows on Postgres. https://docs.dbos.dev
• Restate — durable execution / event-driven services. https://docs.restate.dev
• Inngest — event-driven durable functions. https://www.inngest.com/docs
• Erlang/OTP — actors, supervision trees, let-it-crash. https://www.erlang.org/doc/design_principles/des_princ.html
• Ray — distributed tasks/actors/object store. https://docs.ray.io
• LangGraph — graph state + checkpoints for agents. https://langchain-ai.github.io/langgraph/
• AutoGen — multi-agent conversation framework. https://microsoft.github.io/autogen/
• CrewAI — role-based multi-agent orchestration. https://docs.crewai.com
• MCP — Model Context Protocol (tools/resources/prompts). https://modelcontextprotocol.io
• A2A — Agent2Agent protocol. https://github.com/a2aproject/A2A
• OpenTelemetry — traces/metrics/logs. https://opentelemetry.io/docs/

9.9 可视化与教学参考

• hvmvis — HVM 交互组合子 live playground. https://hvmvis.github.io
• netties — interaction nets / combinators playground. https://netties.adler.dev
• GoI Visualizer — 动态 GoI 机器. https://koko-m.github.io/GoI-Visualiser/
• Interaction Combinator Live — 网页 live. https://hvmvis.github.io
• Bend playground / HVM examples — 语言级 demo. https://github.com/HigherOrderCO/Bend

9.10 阅读顺序建议

1. Lafont 1989 → 2. Lafont 1997 → 3. Lamping 1989 → 4. Gonthier et al. 1992
2. Asperti–Guerrini 1998（选章）→ 6. Mazza 2006（第 1、4、5 章）
3. HVM2 论文 + HVM3 IC.md → 8. Inpla 文档 / Vine 文档
4. 选一个方向深入：最优归约（Lamping/Asperti）、并发（Mazza/multiport）、类型（session）、工程（HVM/Inpla）。

引用规范

• 论文：作者、标题、会议/期刊、年份、链接。
• 代码/项目：仓库链接 + commit/tag（实现时锁定版本）。
• 事实性陈述在 Netbook 中必须带 source；无法核实的说法标记 TODO: verify，不进入正文。

在 GitHub 编辑本文