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.
翻译:在连续功能语言中,大小类型使得能够对具有复杂循环模式的程序进行终止检查,在混合感应-感应类型存在的情况下,这种程序具有复杂的循环模式。在本文中,我们使大小类型及其元神学适应同时的设置。我们将半轴序列计算法扩展为半轴序列计算法,这是基于期货的功能共通货币的子集模式,其基本操作语义带有循环和算术的精细化。后者使得我们能够使用一种新的和高度通用的型号计划,我们称之为规模大小的改进。作为一个广泛应用的技术装置,我们输入具有无穷无穷的打字源衍生法的循环程序,它展示了所有循环电话。然后,我们观察到,某些此类衍生物可以无限宽,但有限度地深。由此产生的树木成为我们终止结果的诱导目标,我们通过新的逻辑关系论来开发。</s>