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.

翻译：在顺序函数式语言中，带大小类型能够在混合归纳-余归纳类型存在的情况下，对具有复杂递归模式的程序进行终止性检查。本文我们将大小类型及其元理论适配到并发场景。我们扩展了半公理sequent演算——一种涵盖基于期货的函数式并发范式的框架——及其底层操作语义，加入了递归与算术精化。后者使我们能够提出一种新型且高度通用的大小类型方案，我们称之为大小类型精化。作为一项广泛适用的技术手段，我们对递归程序进行类型化，使用无穷深的类型推导展开所有递归调用。然后，我们观察到某些此类推导可以变得无限宽但有限深。由此产生的树形结构作为我们终止性结果的归纳目标，我们通过一种新颖的逻辑关系论证对其进行阐述。