Termination in a Pi-calculus with Subtyping

TL;DR

This paper introduces a type system for the pi-calculus that guarantees process termination by leveraging input/output capabilities and subtyping, improving expressiveness and capturing practical programming idioms.

Contribution

It extends existing type systems to accept more terminating processes and demonstrates how to encode the simply typed lambda-calculus within it.

Findings

The system accepts more processes as terminating than previous proposals.

It can encode the simply typed lambda-calculus.

It discusses extensions to handle type inference.

Abstract

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.