Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Single-Threaded Objects

To support efficient execution of certain kinds of models, especially models of microprocessors, ACL2 provides ``single-threaded objects,'' structures with the usual ``copy on write'' applicative semantics but for which writes are implemented destructively. Syntactic restrictions insure consistency between the formal semantics and the implementation. The design of single-threaded objects has been influenced both by the need to make execution efficient and the need to make proofs about them simple. We discuss the issues.

Slides (use "Landscape" when in ghostview)

• One slide per page
• Four slides per page

J Moore