ACL2 Theorem Proving Seminar at the University of Texas

ACL2 stands for ``A Computational Logic for Applicative Common Lisp'' but our research group is interested in all aspects of mechanized theorem proving and in the mechanized verification of hardware and software.

This page lists meetings back to the start of the 2002-2003 academic year.

Click here for some formal methods papers (for possible future presentations).

Upcoming meetings:

Miscellaneous related talks:

Previous meetings (reverse order):

Talks Preceding the 2002-2003 Academic Year

Examples and log from Recursion and Induction class Nov. 1, 2011