Concurrent Realizability on Conjunctive Structures

Emmanuel Beffara (1, 2) , Félix Castro (3, 4) , Mauricio Guillermo (5) , Étienne Miquey (6)

1 MeTAH - Modèles et Technologies pour l’Apprentissage Humain
2 LIG - Laboratoire d'Informatique de Grenoble
3 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
4 PICUBE - Les assistants à la démonstration au cœur du raisonnement mathématique
5 IMERL - Instituto de Matemática y Estadística Rafael Laguardia [Montevideo]
6 I2M - Institut de Mathématiques de Marseille

This work aims at exploring the algebraic structure of concurrent processes and their behaviour independently of a particular formalism used to define them. We propose a new algebraic structure, which we name conjunctive linear algebras, as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in he realm of classical and intuitionistic realizability. In particular, we show how any conjunctive linear algebra provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define the canonical model of this structure as induced by a variant of the π-calculus with global fusions. Using a model of terms, we prove that the parallel composition cannot be defined from the conjunctive structure alone.

Mots clés: Realizability; Process Algebras; Concurrent Programming; Linear Logic

Domaines: Logique en informatique [cs.LO]

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, Étienne Miquey. Concurrent Realizability on Conjunctive Structures. FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. ⟨hal-04083002v1⟩