一句话：提出 F≤μ，将 iso-recursive 类型与有界量化结合，证明子类型可判定、传递且保守，并在 Coq 中形式化。
递归类型与有界量化广泛存在于 Java、C#、Scala 和 TypeScript 等语言中，但二者与子类型的交互长期难以同时获得可判定性、传递性、保守性以及可靠完备的算法化。本文提出 kernel F≤ 的扩展 F≤μ，加入 iso-recursive 类型，并采用新近提出的 nominal unfolding 规则扩展子类型关系。此外，F≤μ 还泛化了 kernel F≤ 的有界量化规则以接受等价边界，并引入受 Abadi、Cardelli 和 Viswanathan 启发的 structural folding/unfolding 规则，从而增强表达力并支持更多应用。作者给出了类型可靠性、子类型的传递性与可判定性、F≤μ 对 F≤ 的保守性，以及可靠完备的算法化子类型判定。文章还研究了带下界量化的扩展 F≤≥μ，且所有结果均已在 Coq 定理证明器中形式化。
Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity and a sound and complete algorithmic formulation has been a long time challenge. This paper presents an extension of kernel F ≤ , called F ≤ µ , with iso-recursive types. F ≤ is a well-known polymorphic calculus with bounded quantification. In F ≤ µ we add iso-recursive types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. We also add two smaller extensions to F ≤ . The first one is a generalization of the kernel F ≤ rule for bounded quantification that accepts equivalent rather than equal bounds. The second extension is the use of so-called structural folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan [1996]. The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity and decidability of subtyping; the conservativity of F ≤ µ over F ≤ ; and a sound and complete algorithmic formulation of F ≤ µ . Moreover, we study an extension of F ≤ µ , called F ≤≥ µ , which includes lower bounded quantification in addition to the conventional (upper) bounded quantification of F ≤ . All the results in this paper have been formalized in the Coq theorem prover.