ACL2 Seminar, Feb. 23, 2011

A Datatype Manager for ACL2 -- A Work in Progress
J Strother Moore

Abstract: Even though ACL2 is an untyped language
most systems of functions implicitly rely on list
structured ``data types.''  I will report on my
recent work to support a succinct language to
declaring such ``types'' and for supporting
reasoning about such types.  The basic approach is
straightforward: use type definitions and declared
signatures to generate ordinary lemmas proved by
ordinary ACL2 means and stored as ordinary ACL2
rules.  Perhaps the most interesting thing about
the whole project is the perspective that it is an
initial prototype at a far grander idea: the
automatic management of rules and rule classes.
This is a work in progress and the system as
implemented so far is far from ready for other
users.