DIRECTORATE OF TIME U.S. Naval Observatory OFFICIAL U.S. TIME

Sunrise is a system for proving programs correct in a feasible way. It contains a deep embedding of a small programming language within the HOL theorem prover, and provides a tool, called a verification condition generator or VCG, for the semi-automatic creation of proofs of total correctness for Sunrise programs within HOL. The VCG is itself verified as sound, and that soundness proof is contained within and checked by the HOL system. This permits the significant simplification of proofs of total correctness of Sunrise programs while retaining complete security.

Higher order quotients may be represented within higher order logic, and their creation has been mechanized within the HOL theorem prover. I am doing research in formal methods for software verification, founded on the semantics of programming languages, where the formal methods are verified by mechanical theorem proving in higher order logic. Interest is growing in the field of formal methods. For a good overview of the current state of formal methods, see Formal Methods: State of the Art and Future Directions, by Ed Clarke and Jeannette Wing, August 1996. It is 22 pages long and has 124 references. And if that's not enough, here are some more links.

My dissertation used the Higher Order Logic (HOL) theorem proving system, (links) as described on the official HOL 4 page, which can be downloaded from Sourceforge. Much information can also be found at Cambridge, or at the Laboratory for Applied Logic at BYU, For a gentler introduction, here is a little page on HOL by Tom Melham. The version of Higher Order Logic most used for research currently is HOL 4, a development and extension of Hol98, written in Moscow ML. Konrad Slind, assisted by Michael Norrish, are the main implementors of HOL. Another major, older version of Higher Order Logic used for research is HOL90, written in Standard ML. Elsa Gunter (old) is the main implementor of HOL90. TkHol by Donald Syme is a graphical user interface to HOL90, with a tutorial and a paper. A great debt is owed three who have contributed substantially to the creation of HOL: Robin Milner, Mike Gordon, and Tom Melham.

Here is some new HOL software I have created to ease defining and working with mutually recursive datatypes, and perform conditional rewriting. This software is free for use.

ANNOUNCEMENT: TPHOLs 2003, the 16th International Conference on Theorem Proving in Higher Order Logics, (bid) will be held in Rome, Italy from Monday, September 9 to Friday, September 13, 2003.

TPHOLs 2002, the 15th International Conference on Theorem Proving in Higher Order Logics, (bid) was held in Hampton, Virginia from Tuesday, August 20 to Friday, August 23, 2002. TPHOLs'2001 (bid) was held in Edinburgh, Scotland in late summer 2001. TPHOLs'2000 was held at the DoubleTree Hotel, Portland, Oregon, August 14 - 18, 2000. (Other logic conferences.)

I graduated in 1995 from UCLA with a Ph.D. in Computer Science. Here is my dissertation, which was only accomplished by God's grace. Soli Deo Gloria. ("To God alone be the glory.") My advisor was Professor David F. Martin. Here is more information about my education. Here are my publications. To avoid automatic search engines taking my email for spam, I have unfortunately had to disguise my email address. To reach me, please use the following, without spaces: