This page is mostly defunct. Most of my ACL2 development has moved into:
- Finite Set Theory based on Ordered Lists (2003/2004)
- A sets library for which uses fully ordered lists. The library provides a great combination of sophisticated reasoning with efficient execution.
- Memories: Array-like Records for ACL2 (2005)
- Efficient implementation of the ACL2 records book for numeric indexes up to some fixed size. Useful for, e.g., representing a processor's memory.
- Unicode File Input (2005/2006)
- A small library which provides some basic support for reasoning about input from files in ACL2, including UTF-8 decoding.
- Miscellaneous ACL2 Stuff
- These are small projects, documentation, useful rules, and so forth. It's all quite random.