Unifying type systems for mobile processes

TL;DR

This paper introduces a unifying framework for process calculus type systems that links functional processes with linear logic proofs, enabling extensions with new features while analyzing their computational properties.

Contribution

It provides a general logical framework unifying various process type systems and explores how adding axioms affects process properties.

Findings

Fragments correspond to known proof-process connections

Adding axioms broadens typeable processes but affects properties

Framework facilitates extending type systems with new features

Abstract

We present a unifying framework for type systems for process calculi. The core of the system provides an accurate correspondence between essentially functional processes and linear logic proofs; fragments of this system correspond to previously known connections between proofs and processes. We show how the addition of extra logical axioms can widen the class of typeable processes in exchange for the loss of some computational properties like lock-freeness or termination, allowing us to see various well studied systems (like i/o types, linearity, control) as instances of a general pattern. This suggests unified methods for extending existing type systems with new features while staying in a well structured environment and constitutes a step towards the study of denotational semantics of processes using proof-theoretical methods.