Trustworthy Tools
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support



The HOL-Omega Logic and Theorem Prover

The HOL-Omega or HOLω system presents a more powerful version of the widely used HOL theorem prover. This system implements a new logic, which is an extension of the existing higher order logic of HOL4. The logic is extended to three levels, adding kinds to the existing levels of types and terms. New types include type operator variables and universal types as in System F. Impredicativity is avoided through the stratification of types by ranks according to the depth of universal types. The HOL-Omega system is a merging of HOL4, HOL2P by Völker, and major aspects of System Fω from chapter 30 of Types and Programming Languages by Pierce. Like HOL4, HOL-Omega is constructed according to the design principles of the LCF approach, for the highest degree of soundness.



Higher Order Quotients

The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, where types are divided by an equivalence relation to create new types, called quotient types. We present a design and an implementation to mechanically construct quotient types as new types in the logic, and to support the automatic lifting of constants and theorems about the original types to corresponding constants and theorems about the quotient types. This design exceeds the functionality of Harrison's package, creating quotients of multiple mutually recursive types simultaneously, and supporting the equivalence of aggregate types, such as lists and pairs. Most importantly, this design supports the creation of higher order quotients, which enable the automatic lifting of theorems with quantification over functions of any higher order.


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.

Making formal methods into normal methods.