Matt Kaufmann
University of Texas at Austin
Logical Foundations for the ACL2 Theorem Prover

ACL2 ("A Computational Logic for Applicative Common Lisp") is a
programming language, a first-order logic, and a software system used
in industry for proving theorems in that logic.  I'll start by giving
an introduction to ACL2.  Then I'll discuss foundational issues for
ACL2.