Aspects of ACL2 User Interaction

Matt Kaufmann, UITP'08, August, 2008

ACL2 ("A Computational Logic for Applicative Common Lisp"):
Joint work by Matt Kaufmann and J Strother Moore, with early contributions from Bob Boyer.

Goal today: Give a sense of how ACL2 supports effective user interaction.

Today we'll touch on numerous aspects of user interaction with ACL2, using small examples to illustrate as time permits. You can obtain a gzipped tar file of the four examples linked to below. Most of the other links below are to topics in the ACL2 documentation.

For fewer examples in a little more depth, see the TPHOLs 2008 ACL2 tutorial.

Narrowest sense of "user interface": Delivering input and output

ACL2 prover output:

Controlling ACL2: