Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors
Matt Kaufmann, J Strother Moore · 2015
Some runtime checks can be safely removed from code if appropriate program properties are proved. We describe how we have applied this idea to the ACL2 theorem prover to speed up the application of user-defined proof procedures. In particular, we discuss how and why we have added a new feature to ACL2 that allows the user to verify certain well-formedness properties of the expressions produced by user-defined proof procedures. Of special interest are the issues of extensibility (how we know that guarantees proved in one theory are adequate in another), formalization of the problem, and design