一句话：为 Wyvern 定义两种路径依赖类型变体，实现可判定类型检查并给出机器验证证明。
路径依赖类型是 Scala 等语言中极具表达力的特性，可建模有界多态、名义子类型以及一等模块。已有工作证明了路径依赖类型在交类型和递归类型下的可靠性，但类型检查仍不可判定，这给依赖类型检查器结果的程序员带来困扰。本文针对面向对象语言 Wyvern（含路径依赖类型、递归类型与一等模块）定义了两个类型检查可判定的变体，并给出机器验证的可判定性证明。尽管引入了限制，这些方法仍能编码 Java 泛型的参数多态以及 Scala 模块系统的许多惯用法。
Path dependent types have long served as an expressive component of the Scala programming language. They allow for the modelling of both bounded polymorphism and a degree of nominal subtyping. Nominality in turn provides the ability to capture first class modules. Thus a single language feature gives rise to a rich array of expressiveness. Recent work has proven path dependent types sound in the presence of both intersection and recursive types, but unfortunately typing remains undecidable, posing problems for programmers who rely on the results of type checkers. The Wyvern programming language is an object oriented language with path dependent types, recursive types and first class modules. In this paper we define two variants of Wyvern that feature decidable typing, along with machine checked proofs of decidability. Despite the restrictions, our approaches retain the ability to encode the parameteric polymorphism of Java generics along with many idioms of the Scala module system.
@article{paperbot554,
title = {Decidable subtyping for path dependent types},
author = {Julian Mackay and Alex Potanin and Jonathan Aldrich and Lindsay Groves},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371134}
}