Light Logics and Higher-Order Processes

TL;DR

This paper applies light logic techniques to process algebras, specifically a restricted Higher-Order pi-calculus inspired by Soft Linear Logic, demonstrating polynomial termination of soft processes and proposing potential extensions.

Contribution

It introduces a soft process calculus inspired by light logics, proving polynomial termination and suggesting ways to extend the class while preserving complexity bounds.

Findings

Soft processes terminate in polynomial time

A restriction of Higher-Order pi-calculus inspired by Soft Linear Logic

Potential for enlarging soft processes class without losing polynomial bounds

Abstract

We show that the techniques for resource control that have been developed in the so-called "light logics" can be fruitfully applied also to process algebras. In particular, we present a restriction of Higher-Order pi-calculus inspired by Soft Linear Logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.