Types for Parallel Complexity in the Pi-calculus

TL;DR

This paper extends type systems to analyze parallel complexity in the pi-calculus, providing bounds on total work and span for concurrent processes using specialized reduction relations and type systems.

Contribution

It introduces two type systems for the pi-calculus that enable extraction of complexity bounds related to parallel computation and communication.

Findings

Defined reduction relations for work and span in pi-calculus

Developed type systems inspired by input/output and size types

Provided a method to derive complexity bounds from typing derivations

Abstract

Type systems as a way to control or analyze programs have been largely studied in the context of functional programming languages. Some of those work allow to extract from a typing derivation for a program a complexity bound on this program. We present how to adapt this result for parallel complexity in the pi-calculus, as a model of concurrency and parallel communication. We study two notions of time complexity: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define reduction relations in the pi-calculus to capture those two notions, and we present two type systems from which one can extract a complexity bound on a process. The type systems are inspired by input/output types and size types, with temporal information about communications.