We present a method to construct "native" type systems for a broad class of languages, in which types are built from term constructors by predicate logic and dependent types. Any language with products and functions can be modelled as a higher-order algebraic theory with rewrites, and the internal language of its presheaf topos provides total specification of the structure and behavior of terms. This construction is functorial, so translations of languages give translations of type systems. The construction therefore provides a shared framework of higher-order reasoning for most existing programming languages.

翻译：我们提出一种方法,为广泛的语言类别构建“本地”类型系统,其中各种类型由术语构建者根据上游逻辑和依附类型构建。 任何具有产品和功能的语言都可以仿照高阶代数理论,并重写,其预写书的内部语言可以提供术语结构和行为的总体规格。这种构建是编剧式,因此语言翻译可以翻译类型系统。 因此,构建为大多数现有程序语言提供了一个更高阶推理的共同框架。