paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Node Replication: Theory And Practice

节点复制：理论与实践
LMCS vol.Volume 20, Issue 12024匹配度 2/10 · 该论文属于纯函数式语言形式语义与求值策略研究，虽与程序语言理论相关，但未涉及用户核心关注的 PL 与 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析等交叉方向。引用 1 inbox
Delia Kesner, Loïc Peyrot, Daniel Ventura
形式语义函数式编程
crossref: 2026-09-10

AI 速览

一句话：提出实现高阶节点复制的项演算，统一刻画按名调用与完全惰性按需调用并证明两者观察等价。

论文研究高阶节点复制的形式化。作者定义并研究一种项演算，用于实现高阶节点复制，并以此统一指定两种弱求值策略：call-by-name 与 fully lazy call-by-need。关键贡献在于借助类型理论工具证明这两种策略观察等价，从而说明在节点复制机制下按名调用与完全惰性按需调用具有相同的可观察行为。该工作为惰性函数式语言中共享与复制的语义及正确性提供了理论依据。

问题
如何形式化高阶节点复制，并比较 call-by-name 与 fully lazy call-by-need 两种弱求值策略的可观察行为。
方法
定义一种实现高阶节点复制的项演算，用其指定两种求值策略，并借助类型理论工具进行推理。
评估
通过类型理论技术证明 call-by-name 与 fully lazy call-by-need 观察等价；论文为理论证明，无实验评估。
原文摘要（Abstract）

We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot2786,
  title = {Node Replication: Theory And Practice},
  author = {Delia Kesner and Loïc Peyrot and Daniel Ventura},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 1},
  year = {2024},
  doi = {10.46298/lmcs-20(1:5)2024}
}