The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens

International audience We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the π-calculus. The introduced model is based on token m...

Full description

Bibliographic Details
Main Authors: Dal Lago, Ugo, Tanaka, Ryo, Yoshimizu, Akira
Other Authors: Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Dipartimento di Scienze dell'Informazione Bologna (DISI), Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO), The University of Tokyo (UTokyo)
Format: Conference Object
Language:English
Published: HAL CCSD 2017
Subjects:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Iceland
Online Access:https://inria.hal.science/hal-01639411
https://inria.hal.science/hal-01639411/document
https://inria.hal.science/hal-01639411/file/main.pdf
Description
Summary:International audience We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the π-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines.

Similar Items