paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Certified, total serialisers with an application to Huffman encoding

可认证的全序列化器及其在 Huffman 编码中的应用
JFP vol.332023匹配度 2/10 · 论文属于定理证明与函数式编程，关注Agda中可认证序列化器与Huffman编码，未涉及用户核心方向：LLM/Agent与静态分析/形式化验证的交叉、浮点程序分析或贝叶斯程序分析。引用 0 inbox
RALF HINZE
定理证明与证明工程函数式编程
crossref: 2026-09-10

AI 速览

一句话：在 Agda 中构造可认证的全序列化器，并以 Huffman 编码作为形式化正确性证明的应用案例。

论文讨论在 Agda 证明助手中构造“可认证”且“全”的序列化器。作者从为 Agda 课程准备应用驱动式教材出发，希望为常见算法给出正确性证明，并以 Huffman 数据压缩作为核心案例。其目标不是只写出能运行的序列化/编码代码，而是让序列化器本身成为全函数，并携带机器检查的正确性保证；Huffman 编码则用于展示这类经认证的序列化器如何落实到具体压缩算法。摘要主要交代了动机与案例背景，技术细节和完整评估未在给出的摘要中展开；从标题与摘要可确认，贡献集中在 Agda 中的机械化正确性证明及其在 Huffman 编码上的应用。

问题
如何在依赖类型证明助手 Agda 中实现既全域（total）又带有正确性认证的序列化器，并以 Huffman 编码说明其实际用途。
方法
采用应用驱动的开发方式，在 Agda 中形式化序列化器并机械化验证其正确性，同时以 Huffman 压缩算法作为案例研究。
评估
评估以 Agda 中机器检查的形式化证明和 Huffman 编码案例为主；摘要未提供实验或基准数据。
原文摘要（Abstract）

The other day, I was assembling lecture material for a course on Agda. Pursuing an application-driven approach, I was looking for correctness proofs of popular algorithms. One of my all-time favourites is Huffman data compression (Huffman, 1952). Even though it is probably safe to assume that you are familiar with this algorithmic gem, a brief reminder of the essential idea may not be amiss.

链接与引用

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

BibTeX 
@article{paperbot2143,
  title = {Certified, total serialisers with an application to Huffman encoding},
  author = {RALF HINZE},
  journal = {Journal of Functional Programming},
  volume = {33},
  year = {2023},
  doi = {10.1017/s095679682200017x}
}