Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator. - Peter V. Homeier; David F. Martin (TPHOLs, 1994)

A Mechanically Verified Verification Condition Generator. - Peter V. Homeier; David F. Martin (Comput. J., 1995)

Mechanical Verification of Mutually Recursive Procedures. - Peter V. Homeier; David F. Martin (CADE, 1996)

Mechanical Verification of Total Correctness through Diversion Verification Conditions. - Peter V. Homeier; David F. Martin (TPHOLs, 1998)

Secure mechanical verification of mutually recursive procedures. - Peter V. Homeier; David F. Martin (Inf. Comput., 2003)

A Design Structure for Higher Order Quotients. - Peter V. Homeier (TPHOLs, 2005)

The HOL-Omega Logic. - Peter V. Homeier (TPHOLs, 2009)