farray:  Field-addressable Arrays in ACL2
Nathan Wetzler
Jan. 27, 2015

Abstract:

State-based models using lists offer poor execution efficiency because
of linear-time operations for reading from and writing to the state.
ACL2 STOBJs (Single-Threaded OBJects) offer better execution
efficiency, but often have poor proof efficiency and proof convenience
for some state-based models.  The farray data structure is an attempt
to improve proof efficiency and proof convenience by embedding scalar
and array fields in a single STOBJ array.  Field read and write
operations work on any field, so modification to a state-based model
is easier than a multi-field STOBJ.