paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Logarithm and program testing

对数与程序测试
POPL 6(POPL)2022匹配度 2/10 · 该论文属于程序语言与类型系统中的多态程序属性测试和单态化理论,不涉及 LLM/Agent、静态分析在 ML/Agentic 系统中的应用,也不涉及浮点程序分析或贝叶斯程序分析,因此与用户研究方向关联较弱。引用 6 inbox
Kuen-Bang Hou (Favonia), Zhuyang Wang
crossref: 2026-09-10

AI 速览

一句话:提出无需嵌入-投影对的机械化单态化,将多态函数用于自动属性测试,并揭示合适类型计算为对数。

随机属性测试近年来备受关注,但多数框架只支持单态属性,对多态属性止步不前。Bernardy 等人曾提出理论将广泛的多态属性归约到单态属性,但依赖 ad-hoc 的嵌入-投影对(embedding-projection pairs)将类型调整成特定形式。本文跳过嵌入-投影对,为一般类多态函数提出一种机械化单态化方法,从而向多态属性的自动测试迈进一步。作者发现,为单态化计算合适类型的过程可归结为对数运算。这一结果简化了多态属性测试的自动化路径,并揭示了类型计算与对数之间的深刻联系。

问题
多态属性的随机属性测试难以自动化,现有归约理论依赖 ad-hoc embedding-projection pairs 调整类型。
方法
跳过 embedding-projection pairs,为一般类多态函数设计机械化单态化,并通过对数运算计算合适的单态类型。
评估
摘要未报告实验评估,主要通过理论构造展示机械化单态化的可行性。
原文摘要(Abstract)

Randomized property-based testing has gained much attention recently, but most frameworks stop short at polymorphic properties. Although Bernardy et al. have developed a theory to reduce a wide range of polymorphic properties to monomorphic ones, it relies upon ad-hoc embedding-projection pairs to massage the types into a particular form. This paper skips the embedding-projection pairs and presents a mechanical monomorphization for a general class of polymorphic functions, a step towards automatic testing for polymorphic properties. The calculation of suitable types for monomorphization turns out to be logarithm .

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1536,
  title = {Logarithm and program testing},
  author = {Kuen-Bang Hou (Favonia) and Zhuyang Wang},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498726}
}