具有类型区间的高阶子类型理论（扩展版）
A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)
摘要：
依赖对象类型（DOT）的演算使Scala的实现更加原则和健壮，但它对类型级计算的支持已被证明是不够的。作为补救措施，我们提出了$F^ω_{..}$，这是Scala的高级类型的严格理论基础。$F^ω_{..}$用区间类扩展了$F^ω_{<:}$，它提供了对Scala中重要的类型级和类级抽象机制的统一处理，例如有界量化、有界运算符抽象、半透明类型定义和第一类子类型约束。其结果是一个灵活的和一般的理论高阶子类型。我们证明了$F^ω_{..}$的类型安全性和类安全性，以及类型的弱规范化和子类型的不可判定性。我们所有的证据是机械化的Agda使用一个完全的语法方法的基础上遗传替代。
英文摘要：
The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose $F^ω_{..}$, a rigorous theoretical foundation for Scala's higher-kinded types. $F^ω_{..}$ extends $F^ω_{<:}$ with interval kinds, which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of $F^ω_{..}$, as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
