Automated Reasoning with Nested Datatypes
Logic in Computer Science
2026-07-01 v1
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.
Cite
@article{arxiv.2606.30888,
title = {Automated Reasoning with Nested Datatypes},
author = {Tomer Hakak and Yoni Zohar and Andrew Reynolds and Clark Barrett and Cesare Tinelli},
journal= {arXiv preprint arXiv:2606.30888},
year = {2026}
}