PrevHomeNext Other Contemplated Talk Titles 
 
This talk is titled
 
Single-Threaded Formal Processor Models: 
Enabling Proof and High-Speed Execution 
 

but we might have called it
 
 

Using ACL2 to Bridge the Gap Between 
Imperative and Functional Programs
 
or
 
 
7 Ways to Build a Toy Processor Model
and Complain about it