ACL2 DEMO GIVEN AT TPHOLs 2008

This is the demo given at TPHOLs 2008 in August, 2008. All files discussed below are available in a gzipped tarfile.

You can also find here a plain text file that served as slides for the talk.

You can view the 5-page proceedings paper, the final version of which has appeared in the TPHOLs 2008 proceedings, with the following bibliographic information. The paper may also be available at http://www.springerlink.com.

@proceedings{tphols2008a,
  editor    = {Otmane Ait Mohamed, César Muñoz and Sofiène Tahar},
  title     = {Theorem Proving in Higher Order Logics, 21th International
               Conference, TPHOLs 2008, Montreal, Canada, August
               18-21, 2008, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5170},
  year      = {2008}
}

The demo consists of the following three parts.

• perm-rev.lisp
  The above file, perm-rev.lisp, contains a demo together with solutions to the various problems encountered when trying to complete the proof. See file perm-rev-exercise.lisp if you want to try working through the demo yourself without the ``answers'', and in the other direction, see file perm-rev-book.lisp for a nice certifiable book based on this demo.

  This demo develops a proof that the reverse of a list is a permutation of the list. It illustrates how to use ACL2 interactively, emphasizing top-down proof development (see :DOC the-method), employing skip-proofs and undoing (see :DOC ubt), and using simplification checkpoints to debug proof failures with gag-mode. This demo also illustrates proof automation using congruence-based conditional rewriting, library development, and local scopes.

• jvm-demo/
  File demo.script in the above directory demonstrates the M5 model of the Java Virtual Machine (JVM). In the process we illustrate several aspects of ACL2. This demo illustrates the use of libraries, packages (see :DOC defpkg) supporting namespaces, efficient evaluation of models, and macros for user-defined syntax (see :DOC defmacro).

• dmr.lisp
  This short demo illustrates management of theories in ACL2 using feedback from the tool, in particular the accumulated-persistence utility and a utility for dynamic monitoring of the rewrite stack.