ACL2

Department of Computer Sciences

1999 ACL2 Workshop

March 29 - March 31, 1999

Suggested ACL2 Enhancements

Our work in developing an executable formal model of the JEM1 gave us an opportunity to explore some of the limits of ACL2, and we have concluded that ACL2 would benefit from three enhancements:

  1. limited inclusion of Common Lisp #.
  2. a new kind of defining event that behaves like a function in the logic but a macro for execution
  3. modular arithmetic execution support
These features would improve ACL2 as a real programming language. In this talk we present examples from our processor modeling that would benefit from the proposed enhancements.

Slides

Examples

David Greve

Last updated March 1999
pete@cs.utexas.edu 		Computer Sciences Department
University of Texas at Austin