Type-Based Incorrectness Reasoning
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914016940523520 |
|---|---|
| author | Zhou, Zhe Delaware, Benjamin Jagannathan, Suresh |
| author_facet | Zhou, Zhe Delaware, Benjamin Jagannathan, Suresh |
| contents | A coverage type generalizes refinement types found in many functional languages with support for must-style underapproximate reasoning. Property-based testing frameworks are one particularly useful domain where such capabilities are useful as they allow us to verify the completeness, as well as safety, of test generators. There is a surprising connection between the kind of underapproximate reasoning coverage types offer and the style of reasoning enabled by recently proposed Incorrectness Logic frameworks. In our presentation, we propose to explore this connection more deeply, identifying mechanisms that more systematically integrate incorrectness reasoning within an expressive refinement type system and the opportunities that such integration offers to functional programmers, program verifiers, and program analyzers and related tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_01511 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Type-Based Incorrectness Reasoning Zhou, Zhe Delaware, Benjamin Jagannathan, Suresh Programming Languages A coverage type generalizes refinement types found in many functional languages with support for must-style underapproximate reasoning. Property-based testing frameworks are one particularly useful domain where such capabilities are useful as they allow us to verify the completeness, as well as safety, of test generators. There is a surprising connection between the kind of underapproximate reasoning coverage types offer and the style of reasoning enabled by recently proposed Incorrectness Logic frameworks. In our presentation, we propose to explore this connection more deeply, identifying mechanisms that more systematically integrate incorrectness reasoning within an expressive refinement type system and the opportunities that such integration offers to functional programmers, program verifiers, and program analyzers and related tools. |
| title | Type-Based Incorrectness Reasoning |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.01511 |