Elementary affine $lambda$-calculus with multithreading and side effects

TL;DR

This paper extends elementary affine lambda calculus with multithreading and side effects, providing termination guarantees, a type system, and demonstrating practical programming of iterative functions within this framework.

Contribution

It introduces a new combinatorial proof of elementary time termination and an affine type system for lambda calculus with multithreading and side effects.

Findings

Termination in elementary time for the extended calculus

A type system ensuring subject reduction and progress

Practical programming of iterative functions with side effects

Abstract

Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side effects focusing on the case of elementary time. Our main contributions are as follows. First, we provide a new combinatorial proof of termination in elementary time for the functional case. Second, we develop an extension of the approach to a call-by-value $lambda$-calculus with multithreading and side effects. Third, we introduce an elementary affine type system that guarantees the standard subject reduction and progress properties. Finally, we illustrate the programming of iterative functions with side effects in the presented formalism.