一句话：提出精化演算 λRF，证明语义子类型与参数多态结合的类型系统可靠性，并在 Liquid Haskell 与 Coq 中机器化元理论。
基于精化类型的实用检查器常结合隐式语义子类型与参数多态，以简化规约并自动验证复杂程序性质，但这类组合的可靠性一直缺乏形式化元理论说明。本文提出核心精化演算 λRF，将语义子类型与参数多态统一起来，建立其元理论并证明类型系统可靠性。为支持机器化，作者引入 data propositions：将归纳定义判断的推导树编码为精化数据类型。随后给出两种机器化：一是用 Liquid Haskell 的精化类型编码元理论，证明其可用于机器化；二是在 Coq 中完整机器化结果，获得比 Liquid Haskell 更强的可靠性保证，为机器化 Liquid Haskell 元理论奠定基础。
Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal metatheoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ R F , a core refinement calculus that combines semantic subtyping and parametric polymorphism. We develop a metatheory for this calculus and prove soundness of the type system. Finally, we give two mechanizations of our metatheory. First, we introduce data propositions , a novel feature that enables encoding derivation trees for inductively defined judgments as refined data types, and use them to show that L iquid H askell ’s refinement types can be used for mechanization. Second, we mechanize our results in C oq , which comes with stronger soundness guarantees than L iquid H askell , thereby laying the foundations for mechanizing the metatheory of L iquid H askell .