"An ACL2 Tutorial."

Matt Kaufmann, J Strother Moore (2008)
a service of Schloss Dagstuhl - Leibniz Center for Informatics