Extended Abstract: Mutable Objects with Several Implementations

This extended abstract outlines an ACL2 feature, attach-stobj 1 , that first appeared in ACL2 Version 8.6 (October, 2024).Familiarity is assumed here with single-threaded objects, or stobjs [1] -not only ordinary concrete stobjs but also abstract stobjs [2].For a worked example that illustrates attach-stobj, see the directory demos/attach-stobj/ in the community books [4], starting with file README.txt in that directory.Performance is addressed in subdirectory mem-test/ of that directory and is discussed in Section 3 below.