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.

翻译：在顺序函数式语言中，带大小类型（sized types）的混合归纳-共归纳类型能够对具有复杂递归模式的程序进行终止检查。本文我们将大小类型及其元理论扩展到并发场景。我们扩展了半公理相继式演算（一种涵盖基于futures的函数式并发计算的范式）及其底层操作语义，引入了递归与算术精化。后者使得一种称为大小类型精化的新型高度通用大小类型方案成为可能。作为广泛适用的技术工具，我们对递归程序进行类型化时，采用展开所有递归调用的无限深度推导树。进一步地，我们观察到某些此类推导可具有无限宽度但有限深度。由此产生的树形结构成为我们终止性结果的归纳目标，我们通过新颖的逻辑关系论证方法对其展开研究。