Document Open Access Logo

Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk)

Authors Elaine Pimentel , Carlos Olarte , Vivek Nigam

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2021.3.pdf
  • Filesize: 0.95 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Process calculi
Keywords
  • Linear logic
  • proof theory
  • process calculi

Metrics

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

Abstract

In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process.

Cite As Get BibTex

Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.3

Author Details

Elaine Pimentel
  • Department of Mathematics, Federal University of Rio Grande Do Norte, Natal, Brazil
Carlos Olarte
  • School of Science and Technology, Federal University of Rio Grande Do Norte, Natal, Brazil
Vivek Nigam
  • Huawei Munich Research Center, Germany

Funding

  • Pimentel, Elaine: Partially funded by the project MOSAIC (MSCA RISE 101007627).
  • Olarte, Carlos: Partially funded by CNPq.

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2(3):297-347, 1992. Google Scholar
  2. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Log., 13(1):2:1-2:44, 2012. Google Scholar
  3. Kaustuv Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In Anuj Dawar and Helmut Veith, editors, CSL 2010, volume 6247 of LNCS, pages 185-199. Springer, 2010. Google Scholar
  4. Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte, and Elaine Pimentel. Hybrid linear logic, revisited. Math. Struct. Comput. Sci., 29(8):1151-1176, 2019. Google Scholar
  5. Kaustuv Chaudhuri and Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, LPAR-20, volume 9450 of LNCS, pages 146-161. Springer, 2015. Google Scholar
  6. Brian F. Chellas. Modal Logic. Cambridge University Press, 1980. URL: https://doi.org/10.1017/CBO9780511621192.
  7. Tiziano Dalmonte, Björn Lellmann, Nicola Olivetti, and Elaine Pimentel. Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. J. Log. Comput., 31(1):67-111, 2021. URL: https://doi.org/10.1093/logcom/exaa072.
  8. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Kurt Gödel Colloquium, volume 713 of LNCS, pages 159-171. Springer, 1993. Google Scholar
  9. Frank S. de Boer, Maurizio Gabbrielli, and Maria Chiara Meo. Proving correctness of timed concurrent constraint programs. ACM Trans. Comput. Log., 5(4):706-731, 2004. Google Scholar
  10. Yuxin Deng, Robert J. Simmons, and Iliano Cervesato. Relating reasoning methodologies in linear logic and process algebra. Math. Struct. Comput. Sci., 26(5):868-906, 2016. Google Scholar
  11. François Fages, Paul Ruet, and Sylvain Soliman. Linear concurrent constraint programming: Operational and phase semantics. Information and Computation, 165(1):14-41, 2001. Google Scholar
  12. Fabio Gadducci, Francesco Santini, Luis Fernando Pino, and Frank D. Valencia. Observational and behavioural equivalences for soft concurrent constraint programming. J. Log. Algebr. Meth. Program., 92:45-63, 2017. Google Scholar
  13. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  14. C. A. R. Hoare. Communications Sequential Processes. Prentice-Hall, Englewood Cliffs (NJ), USA, 1985. Google Scholar
  15. Joxan Jaffar and Michael J. Maher. Constraint logic programming: A survey. J. Log. Program., 19/20:503-581, 1994. Google Scholar
  16. Sophia Knight, Catuscia Palamidessi, Prakash Panangaden, and Frank D. Valencia. Spatial and epistemic modalities in constraint-based process calculi. In Maciej Koutny and Irek Ulidowski, editors, CONCUR, volume 7454 of LNCS, pages 317-332. Springer, 2012. Google Scholar
  17. Björn Lellmann, Carlos Olarte, and Elaine Pimentel. A uniform framework for substructural logics with modalities. In Thomas Eiter and David Sands, editors, LPAR-21, volume 46 of EPiC Series in Computing, pages 435-455. EasyChair, 2017. Google Scholar
  18. Björn Lellmann and Elaine Pimentel. Modularisation of sequent calculi for normal and non-normal modalities. ACM Trans. Comput. Log., 20(2):7:1-7:46, 2019. URL: https://doi.org/10.1145/3288757.
  19. Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451-465. Springer, 2007. Google Scholar
  20. Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theor. Comput. Sci., 294(3):411-437, 2003. Google Scholar
  21. Dale Miller. Hereditary harrop formulas and logic programming. In Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, pages 153-156, Moscow, 1987. Google Scholar
  22. Dale Miller. The pi-calculus as a theory in linear logic: Preliminary results. In Evelina Lamma and Paola Mello, editors, ELP'92, volume 660 of LNCS, pages 242-264. Springer, 1992. Google Scholar
  23. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. Google Scholar
  24. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. Google Scholar
  25. Ugo Montanari. Networks of constraints: Fundamental properties and applications to picture processing. Inf. Sci., 7:95-132, 1974. Google Scholar
  26. M. Nielsen, C. Palamidessi, and F. Valencia. Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing, 9(1):145-188, 2002. Google Scholar
  27. Vivek Nigam. On the complexity of linear authorization logics. In LICS, pages 511-520. IEEE, 2012. Google Scholar
  28. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, Proc. of PPDP'09, pages 129-140. ACM, 2009. Google Scholar
  29. Vivek Nigam and Dale Miller. A framework for proof systems. J. Autom. Reasoning, 45(2):157-188, 2010. Google Scholar
  30. Vivek Nigam, Carlos Olarte, and Elaine Pimentel. A general proof system for modalities in concurrent constraint programming. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR, volume 8052 of Lecture Notes in Computer Science, pages 410-424. Springer, 2013. Google Scholar
  31. Vivek Nigam, Carlos Olarte, and Elaine Pimentel. On subexponentials, focusing and modalities in concurrent systems. Theor. Comput. Sci., 693:35-58, 2017. Google Scholar
  32. Vivek Nigam, Elaine Pimentel, and Giselle Reis. An extended framework for specifying and reasoning about proof systems. J. Log. Comput., 26(2):539-576, 2016. Google Scholar
  33. Carlos Olarte, Davide Chiarugi, Moreno Falaschi, and Diana Hermith. A proof theoretic view of spatial and temporal dependencies in biochemical systems. Theor. Comput. Sci., 641:25-42, 2016. Google Scholar
  34. Carlos Olarte and Elaine Pimentel. On concurrent behaviors and focusing in linear logic. Theor. Comput. Sci., 685:46-64, 2017. Google Scholar
  35. Carlos Olarte, Elaine Pimentel, and Vivek Nigam. Subexponential concurrent constraint programming. Theor. Comput. Sci., 606:98-120, 2015. Google Scholar
  36. Carlos Olarte, Elaine Pimentel, and Camilo Rueda. A concurrent constraint programming interpretation of access permissions. Theory Pract. Log. Program., 18(2):252-295, 2018. Google Scholar
  37. Carlos Olarte, Camilo Rueda, and Frank D. Valencia. Models and emerging trends of concurrent constraint programming. Constraints, 18(4):535-578, 2013. Google Scholar
  38. Elaine Pimentel, Vivek Nigam, and João Neto. Multi-focused proofs with different polarity assignments. In Mario R. F. Benevides and René Thiemann, editors, Proc. of LSFA'15, volume 323 of ENTCS, pages 163-179. Elsevier, 2015. Google Scholar
  39. Elaine Pimentel, Carlos Olarte, and Vivek Nigam. A proof theoretic study of soft concurrent constraint programming. Theory Pract. Log. Program., 14(4-5):649-663, 2014. Google Scholar
  40. V. Saraswat and Martin Rinard. Concurrent constraint programming. In 17th ACM Symp. on Principles of Programming Languages, pages 232-245, San Francisco, CA, 1990. Google Scholar
  41. Vijay A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993. Google Scholar
  42. Vijay A. Saraswat and Martin C. Rinard. Concurrent constraint programming. In Frances E. Allen, editor, POPL, pages 232-245. ACM Press, 1990. Google Scholar
  43. Vijay A. Saraswat, Martin C. Rinard, and Prakash Panangaden. Semantic foundations of concurrent constraint programming. In David S. Wise, editor, POPL, pages 333-352. ACM Press, 1991. Google Scholar
  44. Dana S. Scott. Domains for denotational semantics. In Mogens Nielsen and Erik Meineche Schmidt, editors, ICALP, volume 140 of LNCS, pages 577-613. Springer, 1982. Google Scholar
  45. Ehud Shapiro. The family of concurrent logic programming languages. ACM Comput. Surv., 21(3), 1989. Google Scholar
  46. Gert Smolka. A foundation for higher-order concurrent constraint programming. In J.-P. Jouannaud, editor, Proceedings of Constraints in Computational Logics, volume 845 of LNCS, pages 50-72. Springer-Verlag, 1994. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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