期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：64
页码：44-58
DOI：10.4204/EPTCS.64.4
出版社：Open Publishing Association
摘要：We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system improves over previously existing proposals by accepting more processes as terminating. This increased expressiveness allows us to capture sensible programming idioms. We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.
