Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based process calculus that arises from the Curry-Howard interpretation of the intuitionistic semi-axiomatic sequent calculus and includes unrestricted recursion both at the level of types and processes. With our type refinement system, we can reason about the partial correctness of SAX programs, complementing prior work on sized type refinements that supports reasoning about termination. Our design regime synthesizes the infinitary proof theory of SAX with that of bidirectional typing and Hoare logic, deriving some standard reasoning principles for data and (co)recursion while enabling information hiding for codata. We prove syntactic type soundness, which entails a notion of partial correctness that respects codata encapsulation. We illustrate our language through a few simple examples.

翻译：类型细化将类型检查的组合性与程序逻辑的表达力相结合，为程序验证提供了一种协同方法。本文将依赖类型细化应用于SAX——一种基于未来（futures）的进程演算，该演算源于直觉主义半公理相继式演算的Curry-Howard解释，并在类型和进程层面均支持无限制递归。通过我们的类型细化系统，能够对SAX程序的部分正确性进行推理，补充了先前支持终止性推理的带尺寸（sized）类型细化工作。我们的设计框架将SAX的无穷证明论与双向类型检查和霍尔逻辑相结合，推导出若干面向数据和（余）递归的标准推理原理，同时实现对余数据的信息隐藏。我们证明了类型语义正确性，由此推导出尊重余数据封装的部分正确性概念。最后通过几个简单示例展示了该语言。