The Geometry of Synchronization (Long Version)

TL;DR

This paper extends Girard's Geometry of Interaction by integrating synchronization points through proof-nets for SMLL and a multi-token machine, ensuring deadlock-free execution and linking logical and operational properties.

Contribution

It introduces proof-nets for SMLL with synchronization, and a multi-token machine model that guarantees deadlock-free synchronization, connecting logical correctness with operational behavior.

Findings

Synchronization points are effectively modeled within the Geometry of Interaction framework.

The correctness criterion prevents deadlocks during reduction and execution.

The approach links logical proof structures with operational synchronization mechanisms.

Abstract

We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Interestingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.