• README.html
  this file
• examples.lisp
  a certified book in which we prove the correctness of several byte coded methods, including factorial and point manipulation.
• isort.lisp
  a certified book in which we prove the correctness of the byte code for insertion sort
• perm.lisp
  a certified book dealing with elementary properties of permutation
• script.html
  the html packaging of ACL2 Version 2.5's behavior on script.lisp
• script.lisp
  the script of the demo, showing how to initialize ACL2 and Emacs and then showing every command executed
• script.output
  the ACL2 Version 2.5 output log
• tjvm.lisp
  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 script.lisp.

Matt Kaufmann and J Strother Moore
June, 2000