For the remainder of spring semester 2015, ACL2 seminars will generally take place one hour earlier than usual — namely, on Tuesdays 9:00 am - 10:45 am — in room GDC 7.808 (University of Texas at Austin). This page lists meetings back to the start of the 2002-2003 academic year.
rtl/rel9library, which includes definitions and theorems for reasoning about bit vectors and floating-point operations.
matt.tgz, which extracts to a directory,
matt/, that contains all of the above (see instructions in the
defattachevent for supporting execution of constrained functions, sound modification of system code, and program refinement.
consp, as well as a definitional principle.
support.tar.gz[all of the above]
make-event, which provides the capability to do something like macro-expansion but with access to the ACL2 state and logical world.
http://www.cis.upenn.edu/group/proj/plclub/mmm/. They will also discuss some macros for ACL2 based on ideas from Haskell.
email@example.com of time):
I will talk briefly about staged simplification. Several years ago Pete Manolios and J introduced the notion of stable-under-simplificationp to control rewriting expressions involving a large and detailed machine. Since then, I have found that there is great benefit to be derived by enabling (and subsequently disabling) nonlinear arithmetic under similar control. Both of these are related to the common strategy of examining a failed proof and giving hints at the ``checkpoints''.
http://www.cs.utexas.edu/users/sustik/quantifier-elimination/for slides, papers and references.