A polynomial time {\lambda}-calculus with multithreading and side effects

TL;DR

This paper extends Light Logics to multithreaded programs with side effects, demonstrating polynomial time evaluation, a type system for safety, and expressive concurrent iteration within this framework.

Contribution

It introduces a modal alculus with parallelism and regions, proving polynomial time evaluation and safety for well-formed programs with side effects.

Findings

Call-by-value evaluation is polynomial time for well-formed programs.

A type system guarantees programs do not go wrong.

Expressive concurrent iteration with side effects demonstrated.

Abstract

The framework of Light Logics has been extensively studied to control the complexity of higher-order functional programs. We propose an extension of this framework to multithreaded programs with side effects, focusing on the case of polynomial time. After introducing a modal \lambda-calculus with parallel composition and regions, we prove that a realistic call-by-value evaluation strategy can be computed in polynomial time for a class of well-formed programs. The result relies on the simulation of call-by-value by a polynomial shallow-first strategy which preserves the evaluation order of side effects. Then, we provide a polynomial type system that guarantees that well-typed programs do not go wrong. Finally, we illustrate the expressivity of the type system by giving a programming example of concurrent iteration producing side effects over an inductive data structure.