Semantic-Type-Guided Bug Finding
<|reference_start|>Semantic-Type-Guided Bug Finding: In recent years, there has been an increased interest in tools that establish \emph{incorrectness} rather than correctness of program properties. In this work we build on this approach by developing a novel methodology to prove incorrectness of \emph{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.<|reference_end|>
@article{qian2024semantic-type-guided,
    title={Semantic-Type-Guided Bug Finding},
    author={Kelvin Qian and Scott Smith and Brandon Stride and Shiwei Weng and Ke
  Wu},
    journal={arXiv preprint arXiv:2409.13896},
    year={2024},
    doi={10.1145/3689788},
    archivePrefix={arXiv},
    eprint={2409.13896},
    primaryClass={cs.PL}
}