Automated Reasoning with Nested Datatypes

Tomer Hakak; Yoni Zohar; Andrew Reynolds; Clark Barrett; Cesare Tinelli

doi:10.48550/arxiv.2606.30888

Back

Automated Reasoning with Nested Datatypes

Preprint

Open access

Automated Reasoning with Nested Datatypes

Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett and Cesare Tinelli

ArXiv.org

arXiv

07/01/2026

DOI: 10.48550/arxiv.2606.30888

Files and links (1)

url

https://doi.org/10.48550/arxiv.2606.30888View

Preprint (Author's original) This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging. A decision procedure for the theory is given and proven correct. Finally, we describe an implementation of the procedure, as well as an evaluation over both real-world and crafted benchmarks.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Automated Reasoning with Nested Datatypes
Creators: Tomer Hakak
Yoni Zohar
Andrew Reynolds
Clark Barrett
Cesare Tinelli
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2606.30888
ISSN: 2331-8422
Publisher: arXiv
Language: English
Date posted: 07/01/2026
Academic Unit: Computer Science
Record Identifier: 9985179855402771

Metrics

1 Record Views