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, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

翻译：高阶逻辑HOL提供了一种非常简单的语法和语义，用于表示和推理带类型的数据结构。但其类型系统缺乏类型可能依赖于项的高级特性。依赖类型理论提供了如此丰富的类型系统，但与HOL存在相当显著的概念差异，并且证明自动化支持相对较弱。我们提出了HOL的一种依赖类型扩展DHOL，它保留了HOL的风格和概念框架。此外，我们构建了从DHOL到HOL的翻译，并将其实现为HOL定理证明器的预处理器，从而获得了针对DHOL的定理证明器。