In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our termination result, which we develop via a novel logical relations argument.

翻译：在顺序函数式语言中，尺寸类型能够对包含混合归纳-共归纳类型且具有复杂递归模式的程序进行终止性检查。本文我们将尺寸类型及其元理论扩展到并发场景。我们扩展了半公理相继式演算（一种基于未来型函数式并发性的包容性范式）及其基础操作语义，引入递归与算术精化机制。后者催生了我们称之为"尺寸类型精化"的新型高度泛化尺寸类型方案。作为广泛适用的技术手段，我们通过展开所有递归调用的无穷深度类型推导来标注递归程序。进而发现，某些此类推导可被构造为无限宽度但有限深度的结构。由此产生的树形结构成为我们终止性证明的归纳目标，该证明通过新颖的逻辑关系论证方法完成。