Document Open Access Logo

Concurrent Realizability on Conjunctive Structures

Authors Emmanuel Beffara , Félix Castro , Mauricio Guillermo , Étienne Miquey

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.28.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Author Details

Emmanuel Beffara
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, 38000 Grenoble, France
Félix Castro
  • IRIF, Université Paris Cité, France
  • IMERL, Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay
Mauricio Guillermo
  • IMERL, Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay
Étienne Miquey
  • Aix-Marseille Université, CNRS, I2M, Marseille, France

Funding

This work was partially supported by projects STIC-AmSud Qapla' and APCoRe.

Cite AsGet BibTex

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent Realizability on Conjunctive Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.28

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
Keywords
  • Realizability
  • Process Algebras
  • Concurrent Processes
  • Linear Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. URL: https://doi.org/10.1017/S0960129502003730.
  2. Emmanuel Beffara. Logique, réalisabilité et concurrence. PhD Thesis, Université Paris 7, December 2005. Google Scholar
  3. G. Birkhoff. Lattice theory, volume 25 of Colloquium publications. American Mathematical Society, 1940. Google Scholar
  4. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of ICFP 2000, SIGPLAN Notices 35(9), pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  5. Étienne Duchesne. La localisation en logique : géométrie de l'interaction et sémantique dénotationnelle. Thèse de doctorat, Université Aix-Marseille 2, 2009. URL: http://www.theses.fr/2009AIX22080.
  6. Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, and Alexandre Miquel. Ordered combinatory algebras and realizability. Mathematical Structures in Computer Science, 27(3):428-458, 2017. URL: https://doi.org/10.1017/S0960129515000432.
  7. Yuxi Fu. The χ-Calculus. In 1997 Advances in Parallel and Distributed Computing Conference (APDC), pages 74-81. Computer Society Press, 1997. Google Scholar
  8. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  9. Jean-Yves Girard. Locus Solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, June 2001. URL: https://doi.org/10.1017/S096012950100336X.
  10. Kohei Honda and Nobuko Yoshida. Combinatory representation of mobile processes. In ACM-SIGACT Symposium on Principles of Programming Languages, 1994. Google Scholar
  11. Kohei Honda and Nobuko Yoshida. Replication in concurrent combinators. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 786-805, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  12. J.M.E. Hyland. The effective topos. Studies in Logic and the Foundations of Mathematics, 110:165-216, 1982. The L. E. J. Brouwer Centenary Symposium. URL: https://doi.org/10.1016/S0049-237X(09)70129-6.
  13. J.-L. Krivine. Realizability in classical logic. In Interactive models of computation and program behaviour. Panoramas et synthèses, 27:197-229, 2009. Publisher: Société Mathématique de France. Google Scholar
  14. Jean-Louis Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1):10, February 2012. 28 p. URL: https://doi.org/10.2168/LMCS-8(1:10)2012.
  15. Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing. Mathematical Structures in Computer Science, 30(5):458-510, 2020. URL: https://doi.org/10.1017/S0960129520000079.
  16. Étienne Miquey. Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1-30:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.30.
  17. Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic '09, volume 5771 of Lecture Notes in Computer Science, pages 409-423. Springer, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_30.
  18. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot, 2013. Google Scholar
  19. Joachim Parrow and Björn Victor. The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In 13th IEEE Symposium on Logic in Computer Science (LICS), pages 176-185, 1998. Google Scholar
  20. Andrew M. Pitts. Tripos theory in retrospect. Mathematical Structures in Computer Science, 12(3):265-279, 2002. URL: https://doi.org/10.1017/S096012950200364X.
  21. Davide Sangiorgi and David Walker. The π-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  22. Thomas Streicher. Krivine’s classical realisability from a categorical perspective. Mathematical Structures in Computer Science, 23(6):1234-1256, 2013. URL: https://doi.org/10.1017/S0960129512000989.
  23. Lucian Wischik and Philippa Gardner. Explicit fusions. Theoretical Computer Science, 340(3):606-630, August 2005. URL: https://doi.org/10.1016/j.tcs.2005.03.017.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact