Extended Abstract: Mutable Objects with Several Implementations
Programming Languages
2025-08-04 v1 Logic in Computer Science
Abstract
This extended abstract outlines an ACL2 feature, attach-stobj, that first appeared in ACL2 Version 8.6 (October, 2024). This feature supports different executable operations for a given abstract stobj, without requiring recertification of the book that introduces that stobj or theorems about it. The paper provides background as well as a user-level overview and some implementation notes.
Cite
@article{arxiv.2508.00016,
title = {Extended Abstract: Mutable Objects with Several Implementations},
author = {Matt Kaufmann and Yahya Sohail and Warren A. Hunt},
journal= {arXiv preprint arXiv:2508.00016},
year = {2025}
}
Comments
In Proceedings ACL2 2025, arXiv:2507.18567