Q0 is Peter Andrews' formulation of the simply-typed lambda calculus, and provides a foundation for mathematics comparable to first-order logic plus set theory. It is a form of higher-order logic and closely related to the logics of the HOL theorem prover family.
The theorem proving systems TPS and ETPS are based on Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.[1]