paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A correct-by-construction conversion from lambda calculus to combinatory logic

从 λ 演算到组合子逻辑的正确构造转换
JFP vol.332023匹配度 2/10 · 论文属于纯 PL 理论（λ 演算到组合子逻辑的转换与类型保持），未涉及 LLM/Agent 或静态分析在 AI 系统中的应用，与用户关注的 PL 与 AI 交叉方向不匹配。引用 1 inbox
WOUTER SWIERSTRA
类型系统定理证明与证明工程
crossref: 2026-09-10

AI 速览

一句话：给出从良类型 λ 项到组合子逻辑的转换，并在静态层面同时保证类型保持与转换正确性。

本文提出一个从良类型 λ 演算项到组合子逻辑的转换，目标是在转换过程中同时保证类型保持与转换正确性。与先构造再证明的方式不同，该方法将这两条性质作为构造的内在约束，在静态层面强制成立，从而得到 correct-by-construction 的转换。论文以 pearl 形式展示如何借助精确的类型设计编码转换不变式，使静态检查承担验证职责。关键结果是：对良类型 λ 项，该转换能够产生组合子逻辑项，且类型保持与正确性无需额外手工证明即可得到保证。

问题
如何将良类型 λ 项转换为组合子逻辑项，并同时保证类型保持和转换正确性。
方法
通过静态类型/依赖类型机制将类型保持与正确性编码为转换构造的约束，实现 correct-by-construction 的转换。
评估
评估方式主要是形式化定义与静态类型检查，确保转换对良类型项成立；摘要未明确提及实现或实验评估。
原文摘要（Abstract）

Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.

链接与引用

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

BibTeX 
@article{paperbot2153,
  title = {A correct-by-construction conversion from lambda calculus to combinatory logic},
  author = {WOUTER SWIERSTRA},
  journal = {Journal of Functional Programming},
  volume = {33},
  year = {2023},
  doi = {10.1017/s0956796823000084}
}