Trustworthy Tools
The HOL-Omega Logic and Theorem Prover
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support



The HOL-Omega or HOLω system presents a more powerful version of the widely used HOL4 theorem prover. This system implements a new logic, which is an extension of the existing higher order logic of the HOL4 system. 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.


HOL-Omega is generally described in a briefing (PDF, 21 pages, 12 MB). 


Here is the tutorial for HOL-Omega (PDF, 928 KB). This tutorial is the best way to learn about the HOL-Omega system. It explains both the core features of classic HOL and the new features of HOL-Omega, along with many examples that demonstrate applications of the system. Alternatively, as a short introduction to HOL-Omega, there is a brief teaser for the tutorial (PDF, 202 KB), containing examples that demonstrate in a light way the essential new features of the logic.


The HOL-Omega system is more deeply described in the paper The HOL-Omega Logic (PDF) by Homeier, P.V., in Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs) 2009, LNCS vol. 5674, pp. 244-259. The paper provides examples illustrating and motivating the need for an expanded logic. It presents the abstract syntax and semantics for the ranks, kinds, types, and terms of the logic, as well as the new fundamental axioms and rules of inference.

Despite the value of higher order logic, it has been recognized that there are some useful concepts beyond the power of higher order logic to state. An example is the practical device of monads. Monads are particularly useful in modeling, for example, realistic computations involving state or exceptions, as a shallow embedding in a logic which itself is strictly functional, without state or exceptions. The paper presents examples of using the HOL-Omega system to model monads and prove theorems about their general properties, as well as concepts from category theory such as functors and natural transformations.

The current implementation of the HOL-Omega system differs from that described in the 2009 paper in one major respect. Previously, ranks were attributes of types, as also were kinds. In the current version, ranks are attributes of kinds, and a type's rank is the rank of its kind. The grammar of kinds and types is now as follows:

Kinds: k ::= ty : r | κ : r | k1k2

Types: σ ::= α : kτ : k | σarg σopr | λα.σ | ∀α.σ | ∃α.σ

The parser will accept type annotations of terms (``t : σ``), kind annotations of types (``σ : k``), and rank annotations of kinds (``k : r``).  Rank annotations of types (``σ : r``) are also still accepted.

When deciding if a function term can be properly applied to its argument, the type of the argument must be the type expected by the function, where some difference in ranks is acceptable. As an important innovation, the comparison of types for inequality () depends on whether or not they are classified as humble types. Humble types are types that do not change how they interact with other types as they are promoted to higher rank. In other words, their semantics do not change if their rank is increased. Humble types are defined and described further in an upcoming paper being submitted to ITP 2013.

This change has had no effect on the examples in the 2009 paper or in the example source files in the distribution.


There is a $100.00 bounty available for new soundness bugs discovered in the HOL-Omega kernel. For more details, see here.


The current development version of HOL-Omega is the best version to use.  This is available by using the Git version control system. Git is freely available from here and competently described in the book ProGit by Scott Chacon.
A fresh copy of HOL-Omega may be checked out into a fresh subdirectory called hol-omega by the following Git command: 
git clone -b HOL-Omega git:// hol-omega 
To check out a fresh copy of HOL-Omega that one could edit and write back to the github repository, one would set up a SSH key with github (see here) and then do:
git clone -b HOL-Omega hol-omega
To become an HOL developer and have write access to the github repository, please contact Michael Norrish of NICTA.

The development version is significantly improved over the 2009 release version, and new users are encouraged to use it.

Installation and Implementation

The HOL-Omega theorem prover installs in exactly the same way as the HOL4 theorem prover. Helpful instructions for building HOL4 or HOL-Omega may be found here. Installation instructions are also found in the file INSTALL in the top directory of the downloaded software. HOL-Omega may be built using either the standard or the experimental kernel, and either Moscow ML or Poly/ML, by exactly the same process as for HOL4. Please be aware that building the HOL-Omega system usually takes a few hours, depending on the speed of the computer.
The current implementation is still in development but is already useful. It provides a practical workbench for developments in the HOL-Omega logic, integrated in a natural and consistent manner with the existing HOL4 tools and libraries that have been refined and extended over many years. Examples using the new features of HOL-Omega may be found in the subdirectory examples/HolOmega. Jeremy Dawson of the Australian National University has contributed an advanced exploration of generalized monads and other category theory topics in examples/HolOmega/interim.

The implementation was designed with particular concern for backwards compatibility with HOL4. This was almost entirely achieved, which was possible only because the fundamental data types representing types and terms were originally encapsulated. This meant that the underlying representation could be changed without affecting the abstract view of types and terms by the rest of the system. Virtually all existing HOL4 code will build correctly, including the extensive libraries. The simplifiers have been upgraded, including higher-order matching of the new types and terms and automatic type beta-reduction. Algebraic types with higher kinds and ranks may be constructed using the familiar Hol_datatype tool. Not all of the tools will work as expected on the new terms and types, as the revision process is ongoing, but they will function identically on the classic terms and types. So nothing of HOL4's existing power has been lost.

Making formal methods into normal methods.