2 papers
cs.PL2025
Extended Abstract: Mutable Objects with Several Implementations
Matt Kaufmann, Yahya Sohail, Warren A. Hunt
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…
cs.LO2025
Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2
Matt Kaufmann, J Strother Moore
We illustrate the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2.