Papers and other publications

1. Peter V. Homeier, "The HOL-Omega 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 Springer-Verlag in Lecture Notes in Computer Science volume 5674, pp. 244-259.

2. 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 Springer-Verlag in Lecture Notes in Computer Science volume 3603, pp. 130-146.

3. 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 1-19.

4. 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, Springer-Verlag, pages 189-206.

5. Peter V. Homeier, "Effective Support for Mutually Recursive Types," (PDF), with briefing, (PDF), in ANU Computer Science Technical Report TR-CS-98-08, 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.

6. Carl A. Gunter, Peter Homeier, and Scott Nettles, "Infrastructure for Proof-Referencing Code," (PDF), position paper for the DARPA Workshop on Foundations for Secure Mobile Code, Monterey, California, USA, March 26-28, 1997.

7. Peter V. Homeier and David F. Martin, "Mechanical Verification of Mutually Recursive Procedures," (PDF), in Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 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, Springer-Verlag, pages 201-215.

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

9. 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.

10. 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 19-22, 1994, Lecture Notes in Computer Science Vol 859, Springer-Verlag, pages 269-284.

    Peter V. Homeier, "Satisfaction-Oriented Fuzzy Reasoning," (PDF), presented at the Second International Conference on Fuzzy Theory and Technology, Durham, NC, October 13-16, 1993.

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

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

13. Thach C. Le and Peter V. Homeier, "PORTABLE INFERENCE ENGINE: An Extended CLIPS for Real-Time Production Systems," in Proceedings of the Second Annual Workshop on Space Operations Automation and Robotics, (SOAR '88), July 20-23, 1988, NASA Conference Publication 3019, pages 187-192.

Patents

1. 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.