Termination Analysis for the -Calculus by Reduction to Sequential Program Termination
arXiv:2109.00311
Abstract
We propose an automated method for proving termination of -calculus processes, based on a reduction to termination of sequential programs: we translate a -calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the -calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.
arXiv commentA shorter version will appear in Proceedings of APLAS 2021