Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system but has rather substantial conceptual differences to HOL, including a much more difficult treatment of equality.

We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL while adding the expressivity of dependent types, specifically dependent function types and predicate subtypes. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to the Leo theorem prover for HOL, thereby obtaining a theorem prover for DHOL.