Seminars will generally take place on Tuesdays 4:00 pm - 5:45 pm, in GDC 7.808. This page lists meetings back to the start of the 2002-2003 academic year.
matt.tgz,
which extracts to a directory, matt/, that contains all
of the above (see instructions in the README).defattach event for supporting execution of constrained
functions, sound modification of system code, and program
refinement.defsort book.if, car,
cdr, cons, and consp, as well as a
definitional principle.clock-to-trad.lispdefinition.lispcontradiction.lispsupport.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.
if-tautologyp.
kaufmann@cs.utexas.edu ahead of
time):http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/whats-new/talk.txt.
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''.
go-to-node.tar.gz
http://www.cs.utexas.edu/users/sustik/quantifier-elimination/
for slides, papers and references.