一句话：提出高效易实现的同构递归子类型算法 QuickSub，最坏复杂度 O(nm)，常见情况近线性，并用 Coq 形式化验证。
许多语言需判定两个递归类型是否子类型。递归类型有等递归与同构递归两种建模，现有高效子类型算法多针对等递归，同构递归仍缺乏高效算法。本文提出 QuickSub，一个高效且易实现的同构递归子类型算法，表达力与经典 Amber 规则相同。其最坏复杂度为 O(nm)，其中 m 为类型大小，n 为递归绑定符数量；实际中接近线性，最坏情况难以触发，常见场景下比已有算法快数倍。作者通过经验评估与现有等递归及同构递归算法比较，验证效率；证明算法正确性，并在带递归子类型与记录的简单演算中展示类型可靠性证明。所有结果均在 Coq 中形式化。
Many programming languages need to check whether two recursive types are in a subtyping relation. Traditionally recursive types are modelled in two different ways: equi- or iso- recursive types. While efficient algorithms for subtyping equi-recursive types are well studied for simple type systems, efficient algorithms for iso-recursive subtyping remain understudied. In this paper we present QuickSub : an efficient and simple to implement algorithm for iso-recursive subtyping. QuickSub has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of QuickSub is O ( nm ), where m is the size of the type and n is the number of recursive binders. However, in practice, the algorithm is nearly linear with the worst case being hard to reach. Consequently, in many common cases, QuickSub can be several times faster than alternative algorithms. We validate the efficiency of QuickSub with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms. We prove the correctness of the algorithm and formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness can be proved using QuickSub . All the results have been formalized and proved in the Coq proof assistant.