P2 Binary search—think positive
二分查找——往好处想
JFP vol.352025匹配度 2/10 · 该论文是 Agda 中程序验证的教程，仅以二分查找为例，属于纯形式化验证教学材料，与用户核心关注的 LLM/Agent 和静态分析/形式化验证交叉、浮点或贝叶斯程序分析等方向无直接关联，且无新方法或工业落地内容。引用 0 inbox
ALEXANDER DINGES, RALF HINZE
crossref: 2026-09-10
AI 速览
一句话：在 Agda 中讲解程序验证的教程，并以二分查找为例展开。
本文是一篇关于程序验证的 Agda 教程。根据摘要，其设定为在 Agda 证明助手/依赖类型语言中进行程序验证，具体内容需参考会议议程与附录 A。标题表明教程以二分查找（binary search）为案例，并可能从“正向/积极”的视角组织验证过程。摘要未给出具体的形式化方法、验证性质或实验结果，因此无法进一步判断其技术细节。该文的主要价值在于教学性：展示如何将程序验证技术落到 Agda 中，并通过一个经典算法案例说明证明与实现之间的关系。
- 问题
- 如何在 Agda 中对程序（标题所指的二分查找）进行程序验证，并以教程形式有效讲解；摘要未给出更具体的问题陈述。
- 方法
- 以 Agda 为工具开展程序验证教程，具体方法需参考会议议程和附录 A；标题暗示以二分查找为案例。
- 评估
- 摘要未报告实验或基准评估；呈现形式为教程，评估信息需参见附录 A。
原文摘要（Abstract）
The setting is a tutorial on program verification in Agda. Please consult the programme for further details. [ See also Appendix A .]
链接与引用
DOI 原文 · PDF（开放获取） · DBLP
BibTeX
@article{DingesH25,
title = {Binary search—think positive},
author = {ALEXANDER DINGES and RALF HINZE},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796825000061}
}