Jared Davis
ACL2 Seminar
3/29/2016

I've been working on a fun side project that might make for a
good seminar talk.

The general goal is to develop a fast way to evaluate certain big
integer expressions (which might some day be derived from
hardware descriptions).

The approach is to write and verify a compiler that can
(statically) compile away the details of the bigint operations
into the usual 64-bit operations that are available in LLVM
assembly code.  The assembly code can then be compiled (by LLVM)
into an executable or shared library and used in external
programs or reloaded into ACL2 itself.

This is still exploratory prototyping and there are definitely
missing pieces.  But much is shaping up and there are a lot of
neat components coming out of it (verified bigint operations,
some generic DAG algorithm proofs, connecting to shared libraries
from ACL2 with CFFI, etc).