Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2409.13896 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912039368130560 |
|---|---|
| author | Qian, Kelvin Smith, Scott Stride, Brandon Weng, Shiwei Wu, Ke |
| author_facet | Qian, Kelvin Smith, Scott Stride, Brandon Weng, Shiwei Wu, Ke |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_13896 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Semantic-Type-Guided Bug Finding Qian, Kelvin Smith, Scott Stride, Brandon Weng, Shiwei Wu, Ke Programming Languages 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. |
| title | Semantic-Type-Guided Bug Finding |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2409.13896 |