标题：Formalizing, Mechanizing, and Verifying Class-based Refinement Types

作者：孙可、王迪*、Sheng Chen、Meng Wang、郝丹

摘要：精化类型系统已在基于类的面向对象语言中广泛用于表述和验证细粒度的逻辑规约。尽管在实际的适用性和可用性方面取得了进展，这些精化类型系统仍存在两个基本问题。一方面，现有基于类的精化类型系统的soundness缺乏研究，这使得其可靠性成为了问题。另一方面，这些系统的表达能力有限，限制了与面向对象构造相关的语义属性的描述。本工作通过一个系统化的框架解决了这些问题。我们形式化了一个声明式的基于类的精化类型演算RFJ，该演算表达性强并且形式上是简洁的。我们严格地设计了这个演算的元理论，并将其在Coq形式化，证明了其soundness。为了确保演算的可验证性，我们提出了基于一个一阶逻辑的子集LFJ的验证算法，并将这种方法实现为了一个自动类型检查工具。