DBLP list of my publications

My copies of the pdfs (The original publication is available at www.springerlink.com)

• Challenges in using OpenTheory to Transport Harrison's Model from HOL Light to HOL4
• Steps Towards Verified Implementations of HOL Light
• Standalone Tactics using OpenTheory
• Validating QBF Invalidity in HOL4 (also see Tjark Weber's copy)
• Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study
• (Nominal) Unification by Recursive Descent with Triangular Substitutions