paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Separation logic for sequential programs (functional pearl)

顺序程序的分离逻辑（functional pearl）
ICFP 4(ICFP)2020匹配度 3/10 · 论文属于程序验证/分离逻辑的形式化基础工作，与用户'AI→PL 用 LLM/Agent 改进静态分析与形式化验证'的方向仅有间接的领域重叠，完全不涉及 LLM、Agent、浮点或贝叶斯程序分析；且其为教学导向的 functional pearl，缺乏新方法与工程落地/benchmark 价值。引用 34 inbox
Arthur Charguéraud
程序验证定理证明与证明工程
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话：提出面向顺序程序分离逻辑的简易机器化形式化，用于教学并覆盖可靠性证明与近期扩展。

本文针对分离逻辑教学缺乏简单且可机器检验的形式化材料这一问题，提出了一个面向顺序程序的分离逻辑形式化。该形式化以教学为目标，覆盖分离逻辑的核心思想、可靠性证明以及若干近期增强，并采用与 Software Foundations 系列类似的课程组织方式，所有命题与证明均在 Coq 中形式化。其设计只假定读者具备 lambda 演算、语义学和逻辑学的基础知识，因此适合广泛受众。作为 functional pearl，它强调简洁性与可读性，可作为课程支撑与入门参考。

问题
如何以简单、可机器检验的方式形式化顺序程序的分离逻辑，并使其适合教学，覆盖可靠性证明与近期增强。
方法
在 Coq 中机器化形式化分离逻辑，采用类似 Software Foundations 的课程式组织，所有陈述和证明均被形式化。
评估
通过 Coq 机械化验证相关陈述与证明，并作为课程支撑材料，以低前置知识要求保证广泛可访问性。
原文摘要（Abstract）

This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of lambda-calculus, semantics and logics, and therefore should be accessible to a broad audience.

链接与引用

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

BibTeX 
@article{Chargueraud20,
  title = {Separation logic for sequential programs (functional pearl)},
  author = {Arthur Charguéraud},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {ICFP},
  year = {2020},
  doi = {10.1145/3408998}
}