5 citations · 18 across the 5 of their papers we have counts for
5 papers
Iteration in ACL2
Matt Kaufmann, J Strother Moore
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- pro…
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
J. Strother Moore
When ACL2 is used to model the operational semantics of computing machines, machine states are typically represented by terms recording the contents of the state components. When m…
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
Matt Kaufmann, J Strother Moore
We report on improvements to ACL2 made since the 2013 ACL2 Workshop.
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1
Matt Kaufmann, J Strother Moore
We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we f…
How Can I Do That with ACL2? Recent Enhancements to ACL2
Matt Kaufmann, J Strother Moore
The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-e…