我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：该文是《使用 Coq 证明助手推理递归程序的折叠-展开引理》的勘误，摘要不可用，无法概括新贡献。

该条目是 Olivier Danvy 关于《使用 Coq 证明助手推理递归程序的折叠-展开引理》的勘误（ERRATUM）。给出的摘要字段明确说明此内容没有可用的摘要；页面仅提供完整 HTML 内容，并提供通过“Save PDF”按钮获取 PDF。因此，仅根据标题、作者和摘要，无法获知原文的问题设定、采用的方法、评估方式以及关键结果，也无法判断勘误具体修正了哪些内容。此处只能记录文献类型为勘误，主题涉及使用 Coq 证明助手对递归程序进行推理的折叠-展开引理。若需结构化速览，应获取并阅读全文。

问题

给出的摘要不可用，无法确定原文研究问题；标题提示其主题为使用 Coq 证明助手推理递归程序。

方法

摘要未提供，无法确定具体方法；从标题看可能涉及 Coq 中的折叠-展开引理，但这仅为题名信息。

评估

摘要未提供，无法判断评估方式；该条目本身为勘误，未给出可评估内容。

链接与引用

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

@article{paperbot2142,
  title = {Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant – ERRATUM},
  author = {OLIVIER DANVY},
  journal = {Journal of Functional Programming},
  volume = {33},
  year = {2023},
  doi = {10.1017/s0956796823000011}
}