Towards computer-verified proofs of correctness of logic-programming interpreters using derivations
Vernon Austel, D. Stott Parker · 1997
This thesis presents sixteen increasingly refined kinds of derivations and proves that they are equivalent using the HOL proof checker; the first is close to the common one (such as given by Lloyd), while the last is expressed using abstract machine states modeled after the Warren Abstract Machine (WAM). The concept of derivation has never been refined like this in the verification literature. We use these versions of derivation in the first part of a proof of correctness by refinement stages for a simple version of the WAM. Much of the complexity of the WAM is due to details concerning the representation of data (terms and substitutions). We argue that it is simpler to refine data representation before control, and that backtracking should be refined last. Our refinement technique should be applicable to other logic-programming languages such as full Prolog.