An affine-intuitionistic system of types and effects: confluence and termination

TL;DR

This paper introduces an affine-intuitionistic type system for multi-threaded programs with effects, ensuring confluence and termination through region usage discipline and stratification.

Contribution

It extends Dual Intuitionistic Linear Logic to handle multi-threaded effects with a novel region-based discipline for confluence and termination guarantees.

Findings

Region usage discipline ensures program confluence.

Region stratification guarantees termination.

The system models references and channels with finite regions.

Abstract

We present an affine-intuitionistic system of types and effects which can be regarded as an extension of Barber-Plotkin Dual Intuitionistic Linear Logic to multi-threaded programs with effects. In the system, dynamically generated values such as references or channels are abstracted into a finite set of regions. We introduce a discipline of region usage that entails the confluence (and hence determinacy) of the typable programs. Further, we show that a discipline of region stratification guarantees termination.