{"ID":2890356,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.00016","arxiv_id":"2508.00016","title":"Extended Abstract: Mutable Objects with Several Implementations","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.","short_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 back...","url_abs":"https://arxiv.org/abs/2508.00016","url_pdf":"https://arxiv.org/pdf/2508.00016v1","authors":"[\"Matt Kaufmann\",\"Yahya Sohail\",\"Warren A. Hunt\"]","published":"2025-07-25T07:07:52Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.LO\"]","methods":"[]","has_code":false}