
Peter V. Homeier,
"The HOLOmega Logic"
(PDF).
Presentated as a paper in the Mature Work Category at TPHOLs 2009,
the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany,
August 17  20, 2009.
Proceedings published by SpringerVerlag in
Lecture Notes in Computer Science volume 5674,
pp. 244259.

Peter V. Homeier,
"A Design Structure for Higher Order Quotients"
(PDF).
Presentated as a paper in the Mature Work Category at TPHOLs 2005,
the 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK,
August 22  25, 2005.
Proceedings published by SpringerVerlag in
Lecture Notes in Computer Science volume 3603,
pp. 130146.

Peter V. Homeier and David F. Martin,
"Secure mechanical verification
of mutually recursive procedures,"
Information and Computation,
Vol. 187, Issue 1, November 25, 2003, Elsevier, pages 119.

Peter V. Homeier and David F. Martin,
"Mechanical Verification of Total Correctness
Through Diversion Verification Conditions,"
(PDF), with
briefing,
(PDF),
in Proceedings of the
11th International Conference on
Theorem Proving in Higher Order Logics (TPHOLs'98),
eds. J. Grundy and M. Newey,
The Australian National University (ANU),
Canberra, Australia,
September 28  October 1, 1998.
Lecture Notes in Computer Science Vol 1479,
SpringerVerlag, pages 189206.

Peter V. Homeier,
"Effective Support for Mutually Recursive Types,"
(PDF), with
briefing,
(PDF), in
ANU
Computer Science Technical Report TRCS9808,
Theorem Proving in Higher Order Logics: Emerging Trends 
Proceedings of the 11th International Conference,
TPHOLs'98, Canberra, Australia, September  October 1998,
Supplementary Proceedings,
eds. Jim Grundy and Malcolm Newey,
September 1998, updated in October 1998.

Carl A. Gunter, Peter Homeier, and Scott Nettles,
"Infrastructure for ProofReferencing Code,"
(PDF),
position paper for the
DARPA Workshop on Foundations for Secure Mobile Code,
Monterey, California, USA, March 2628, 1997.

Peter V. Homeier and David F. Martin,
"Mechanical Verification of Mutually Recursive Procedures,"
(PDF),
in Proceedings of the 13th International Conference
on Automated Deduction (CADE13),
eds. M. A. McRobbie and J. K. Slaney,
Rutgers University, New Brunswick, NJ, USA,
July 30  August 3, 1996,
Lecture Notes in Artificial Intelligence Vol 1104,
SpringerVerlag, pages 201215.

Peter V. Homeier and David F. Martin,
"A Mechanically Verified Verification Condition Generator,"
(PDF),
The Computer Journal,
Vol. 38, No. 2, July 1995, pages 131141.

Peter V. Homeier,
Trustworthy Tools for Trustworthy Programs:
A Mechanically Verified Verification Condition Generator
for the Total Correctness of Procedures, (Ph.D. Dissertation),
Department of Computer Science, University of California,
Los Angeles, June 1995.

Peter V. Homeier and David F. Martin,
"Trustworthy Tools for Trustworthy Programs:
A Verified Verification Condition Generator,"
(PDF),
in Proceedings of the 7th International Workshop
on Higher Order Logic Theorem Proving and its Applications,
eds. Thomas Melham and Juanito Camilleri, Valletta, Malta,
September 1922, 1994,
Lecture Notes in Computer Science Vol 859,
SpringerVerlag, pages 269284.
Peter V. Homeier,
"SatisfactionOriented Fuzzy Reasoning,"
(PDF),
presented at the Second International Conference on Fuzzy Theory
and Technology, Durham, NC, October 1316, 1993.

Peter V. Homeier, Thach C. Le, Y. Peter Li, and Peter C. Eggan,
"DEFCLIPS: Extensions to the CLIPS Production System Environment,"
in Proceedings of Artificial Intelligence/Expert Systems
Symposium, El Segundo, CA, September 12, 1993.

Peter V. Homeier and Thach C. Le,
"ECLIPS: An Extended CLIPS for Backward Chaining and GoalDirected
Reasoning,"
(PDF),
in Proceedings
of the Second CLIPS Users Group Conference, September 2325,
1991, Houston, Texas, NASA Conference Publication 10085, Volume 2,
pages 213225. Here is the system's
source code.

Thach C. Le and Peter V. Homeier, "PORTABLE INFERENCE ENGINE:
An Extended CLIPS for RealTime Production Systems," in
Proceedings of the Second Annual Workshop on Space Operations
Automation and Robotics, (SOAR '88), July 2023, 1988, NASA
Conference Publication 3019, pages 187192.
Patents

U.S. Patent for
Method for Verifying the Total Correctness
of a Program With Mutually Recursive Procedures,
U.S. Patent No. 5,963,739,
issued October 5, 1999.

