一句话：提出语义类型反驳器，借助符号求值证明函数式程序的语义类型性质不成立，从而发现类型错误。
近年来，旨在证明程序性质不成立（incorrectness）而非成立的工具受到越来越多关注。本文延续这一思路，将其推广到函数式程序类型系统的模型论：作者为一个简单的函数式语言定义了「语义类型反驳器」（semantic type refuter），用于反驳语义类型断言。论文证明了该反驳器是余递归可枚举的（co-recursively enumerable），并相对于某一语义类型概念既是可靠的又是完备的。作者还给出了一个初步实现，该实现通过符号求值在具有丰富类型系统的函数式语言中高效地搜索类型错误。
In recent years, there has been an increased interest in tools that establish incorrectness rather than correctness of program properties. In this work we build on this approach by developing a novel methodology to prove incorrectness of semantic typing properties of functional programs, extending the incorrectness approach to the model theory of functional program typing. We define a semantic type refuter which refutes semantic typings for a simple functional language. We prove our refuter is co-recursively enumerable, and that it is sound and complete with respect to a semantic typing notion. An initial implementation is described which uses symbolic evaluation to efficiently find type errors over a functional language with a rich type system.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2409-13896,
title = {Semantic-Type-Guided Bug Finding},
author = {Kelvin Qian and Scott Smith and Brandon Stride and Shiwei Weng and Ke Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689788}
}