Concurrent Realizability on Conjunctive Structures
| Autor: | Beffara, Emmanuel, Castro, Félix, Guillermo, Mauricio, Miquey, Étienne |
|---|---|
| Přispěvatelé: | Modèles et Technologies pour l’Apprentissage Humain (MeTAH ), Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Les assistants à la démonstration au cœur du raisonnement mathématique (PICUBE), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Instituto de Matemática y Estadística Rafael Laguardia [Montevideo] (IMERL), Universidad de la República [Montevideo] (UDELAR), Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), This work was partially supported by projects STIC-AmSud Qapla’ and APCoRe |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction FSCD 2023-8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy |
| Popis: | This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA 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 a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone. LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 28:1-28:21 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|