Title: An Integration of Axiomatic Set Theory with ACL2
Speaker: Matt Kaufmann

Abstract:

This work in progress supports the use of ACL2 to reason both about
set theory and about "higher-order" notions (without involving
apply$).  It resides in the community books directory,
books/projects/set-theory/.

I'm planning on giving two or three 90-minute talks over Zoom, all of
them informal with questions encouraged.  They will include the basics
of what can be done with these books as well as a sketch of their
logical foundations.  The talks will also likely discuss somewhat
uncommon ACL2 techniques that may be of use in other ACL2 projects.

More information on this work in progress is available from the
documentation:

https://www.cs.utexas.edu/~moore/acl2/manuals/latest/?topic=ACL2____ZFC
https://www.cs.utexas.edu/~moore/acl2/manuals/latest/?topic=ACL2____ZFC-MODEL

-- Matt