Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures.

We describe a sound method for permitting the users of a mechanical theorem-proving system to add executable code to the system, thereby implementing a new proof strategy and modifying the behavior of the system. The new code is mechanically derived from a function definition conceived by the user but proved correct by the system before the new code is added. We present a simple formal method for stating within the theory of the system the correctness of such functions. The method avoids the complexity of embedding the rules of inference of the logic in the logic. Instead, we define a meaning function that maps from objects denoting expressions to the values of those expressions under a given assignment. We demonstrate that if the statement of correctness for a given 'metafunction' is proved, then the code derived from function's definition can be used as a new proof procedure. We explain how we have implemented the technique so that the actual application of a metafunction is as efficient as hand-coded procedures in the implementation language. We prove the correctness of our implementation. We discuss a useful metafunction that our system has proved correct and now uses routinely. We discuss the main obstacle to the introduction of metafunctions: proving them correct by machine. (Author)