This is the README file for the ACL2 flying demo. The relevant files on this
a certified book in which we prove the correctness of several byte coded methods, including factorial and point manipulation.
a certified book in which we prove the correctness of the byte code for insertion sort
a certified book dealing with elementary properties of permutation
the html packaging of ACL2 Version 2.5's behavior on script.lisp
the script of the demo, showing how to initialize ACL2 and Emacs and then showing every command executed
the ACL2 Version 2.5 output log
a certified book defining a toy Java Virtual Machine.
If you wish to reproduce the demo on your local copy of ACL2, you should retrieve each
of these files. Then certify the books noted above; certification instructions are
included in each book. Then carry out the instructions in
Matt Kaufmann and J Strother Moore