Memories: Array-like Records for ACL2

ArrayMemories

This is an ACL2 library for modelling fixed-size arrays and linear memories, which features:

  • The same rules as misc/records
  • Optimized O(log n) operations
  • Good space efficiency
  • No STOBJs or ACL2 arrays

This library is free software released under the terms of the GNU General Public License.

Download

Download memory-0.31.tar.gz
GZipped Tar File; 27 KB
Note: You may already have this library installed. It is distributed in the books/data-structures directory of ACL2 3.0.

Documentation

PDF Memories: Array-like Records for ACL2
To appear in ACL2 '06
PDF; 92 KB

Presentations

Movie ACL2 '06 Movie
WMV; 12 MB; 11 Minutes
PDF ACL2 '06 Slides
PDF; 209 KB
This is the presentation for ACL2 '06. It's a short, high-level introduction to the library.
PDF October 2005 ACL2 Seminar Slides
PDF; 2.5 MB
This is a much more detailed presentation from a 10/12/2005 talk at the Weekly ACL2 Seminar at UT.

Development

Code Browse Source (stable version)
This just gives you the Apache file listing.
Code Browse Subversion (development version)
Note that this viewer can be pretty slow.
Anonymous SVN access is also available, e.g., svn checkout svn://dimebox.cs.utexas.edu/u/jared/Subversion/memory/trunk memory