|
|
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.
(Details)
|
|
|
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
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.
|
