John Harrison: Towards Self-verification of HOL Light. IJCAR 2006: 177-191