D.  Pedreschi and Ruggieri, S., ?A Case Study in Logic Program Verification: the Vanilla Metainterpreter?, in GULP-PRODE, 1995, pp. 643-654.