Matt Kaufmann
ACL2: Implementation of a Computational Logic

ACL2 ("A Computational Logic for Applicative Common Lisp") is a
programming language, a first-order logic, and a software system for
proving theorems in that logic.  In this talk I will give logicians a
sense of what ACL2 is, what can be done with it, and especially what
sorts of logical issues can arise when attempting to build a powerful
yet sound mechanized reasoning system.