机械化细化类型（扩展版）
摘要：通过细化类型基于模型检验的实际检查器，使用隐式语义子类型和参数化多态性的组合来简化程序的规范并自动化验证复杂的属性。然而，使用这种组合的细化类型系统的形式元理论的准确性验证一直是困难的。我们介绍lambda_RF，它是一个结合了语义子类型和参数化多态性的核心细化演算。我们为此演算开发了元理论，并证明了类型系统的准确性。最后，我们使用基于细化类型的LiquidHaskell作为证明检查器，对我们的元理论进行了完整的机械化，展示了细化类型如何用于机械化。
作者：Michael Borkowski, Niki Vazou, Ranjit Jhala
论文ID：2207.05617
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-13