Parallelism and Synchronization in an Infinitary Context (Long Version)

TL;DR

This paper introduces multitoken interaction machines within a highly expressive logical framework, demonstrating deadlock-free interaction and the ability to embed PCF, thus bridging low-level implementation models with high-level programming language semantics.

Contribution

It develops a new multitoken interaction machine model for a complex logical system, ensuring deadlock freedom and accurate PCF embedding, surpassing single-token models.

Findings

Interaction is guaranteed to be deadlock free.

The logical system can embed PCF for both call-by-name and call-by-value.

Multitoken machines provide a closer link to low-level implementation.

Abstract

We study multitoken interaction machines in the context of a very expressive logical system with exponentials, fixpoints and synchronization. The advantage of such machines is to provide models in the style of the Geometry of Interaction, i.e., an interactive semantics which is close to low-level implementation. On the one hand, we prove that despite the inherent complexity of the framework, interaction is guaranteed to be deadlock free. On the other hand, the resulting logical system is powerful enough to embed PCF and to adequately model its behaviour, both when call-by-name and when call-by-value evaluation are considered. This is not the case for single-token stateless interactive machines.