Matt Kaufmann (joint work with J Moore)
ACL2 Seminar, April 19, 2019

I will give two short talks today.

==================== Talk #1 ====================

Title: Iteration in ACL2

Abstract:
Iterative algorithms are traditionally expressed in ACL2 using
recursion.  On the other hand, Common Lisp provides a construct,
LOOP, which --- like most programming languages --- provides direct
support for iteration.  We describe an ACL2 analogue LOOP$ of LOOP
that supports efficient ACL2 programming and reasoning with iteration.

==================== Talk #2 ====================

Title: What's New in ACL2 Version 8.2

Abstract:
The next ACL2 release, Version 8.2, is scheduled to appear next month.
More than 50 ACL2 enhancements, all made after the Version 8.1 release
last September, are reported in the corresponding release notes (:DOC
note-8-2).  In this talk I will discuss a few of these.