论文标题
高调类型（扩展）
Mechanizing Refinement Types (extended)
论文作者
论文摘要
基于改进类型的实用检查器使用隐式语义亚型和参数多态性的组合来简化规范并自动化程序的复杂属性验证。但是，使用这种组合对改进类型系统的健全性进行正式的元理论核算被证明是难以捉摸的。我们提出λ_rf核心细化计算，结合了语义亚型和参数多态性。我们为这种微积分开发了一种元理论，并证明了类型系统的健全性。最后，我们使用基于改进型的LiquidHaskell作为证明检查器提供了元理论的完整机械化，显示了如何将改进用于机械化。
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF a core refinement calculus that combines semantic sub-typing and parametric polymorphism. We develop a meta-theory for this calculus and prove soundness of the type system. Finally, we give a full mechanization of our meta-theory using the refinement-type based LiquidHaskell as a proof checker, showing how refinements can be used for mechanization.
