Document Open Access Logo

Private Names in Non-Commutative Logic

Authors Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.31.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Ross Horne
Alwen Tiu
Bogdan Aman
Gabriel Ciobanu

Cite AsGet BibTex

Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. Private Names in Non-Commutative Logic. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.31

Abstract

We present an expressive but decidable first-order system (named MAV1) defined by using the calculus of structures, a generalisation of the sequent calculus. In addition to first-order universal and existential quantifiers the system incorporates a de Morgan dual pair of nominal quantifiers called `new' and `wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of the operators `new' and `wen' is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. Modelling processes as predicates in MAV1 has the advantage that linear implication defines a precongruence over processes that fully respects causality and branching. The transitivity of this precongruence is established by novel techniques for handling first-order quantifiers in the cut elimination proof.
Keywords
  • process calculi
  • calculus of structures
  • nominal logic
  • causal consistency

Metrics

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

References

  1. Luca Aceto and Matthew Hennessy. Adding action refinement to a finite process algebra. Information and Computation, 115(2):179-247, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1096.
  2. Andrei Alexandru and Gabriel Ciobanu. Nominal techniques for π I-calculus. Romanian Journal of Information Science and Technology, 16(4):261-286, 2013. Google Scholar
  3. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. URL: http://dx.doi.org/10.1093/logcom/2.3.297.
  4. Marek Bednarczyk. Hereditary history preserving bisimulations. Technical report, Polish Academy of Sciences, Gdańsk, 1991. Google Scholar
  5. Kai Brünnler. Deep inference and symmetry in classical proofs. PhD thesis, TU Dresden, 2003. Google Scholar
  6. Kai Brünnler. Locality for classical logic. Notre Dame J. Form. Log., 47(4):557-580, 2006. Google Scholar
  7. Paola Bruscoli. A purely logical account of sequentiality in proof search. In ICLP, volume 2401 of LNCS, pages 302-316. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45619-8_21.
  8. Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic (TOCL), 10(2), 2009. URL: http://dx.doi.org/10.1145/1462179.1462186.
  9. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR 2010, pages 222-236. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_16.
  10. Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In EACSL, volume 12, pages 159-173, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159.
  11. Gabriel Ciobanu and Ross Horne. Non-interleaving operational semantics for geographically replicated databases. In SYNASC 2013, pages 440-447, 2013. URL: http://dx.doi.org/10.1109/SYNASC.2013.64.
  12. Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In PSI 2015, 25-27 August, Kazan, Russia, volume 9609 of LNCS, 2015. Google Scholar
  13. Murdoch J. Gabbay. The π-calculus in FM. In Thirty Five Years of Automating Mathematics, pages 247-269. Springer, 2003. URL: http://dx.doi.org/10.1007/978-94-017-0253-9_10.
  14. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. URL: http://dx.doi.org/10.1016/j.ic.2010.09.004.
  15. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-112, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  16. Alessio Guglielmi. Re:encoding pi calculus in calculus of structures. post on public mailing list http://permalink.gmane.org/gmane.science.mathematics.frogs/161, 2004.
  17. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1), 2007. URL: http://dx.doi.org/10.1145/1182613.1182614.
  18. Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: The exponentials and splitting. Math. Struct. Comp. Sci., 21(03):563-584, 2011. URL: http://dx.doi.org/10.1017/S096012951100003X.
  19. Kohei Honda et al. Scribbling interactions with a formal foundation. In ICDCIT 2011, volume 6536 of LNCS, pages 55-75. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19056-8_4.
  20. Ross Horne. The consistency and complexity of multiplicative additive system virtual. Sci. Ann. Comp. Sci., 25(2):245-316, 2015. URL: http://dx.doi.org/10.7561/SACS.2015.2.245.
  21. Naoki Kobayashi and Akinori Yonezawa. ACL - a concurrent linear logic programming paradigm. In ILPS'93, pages 279-294. MIT Press, 1993. Google Scholar
  22. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. URL: http://dx.doi.org/10.1145/359545.359563.
  23. Patrick Lincoln and Natarajan Shankar. Proof search in first-order linear logic and other cut-free sequent calculi. In LICS'94, pages 282-291. IEEE, 1994. URL: http://dx.doi.org/10.1109/LICS.1994.316061.
  24. José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73-155, 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90182-F.
  25. Dale Miller and Alwen Tiu. A proof theory for generic judgements. ACM Transactions on Computational Logic (TOCL), 6(4):749-783, 2005. URL: http://dx.doi.org/10.1145/1094622.1094628.
  26. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1-77, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  27. Peter O'Hearn and David Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: http://dx.doi.org/10.2307/421090.
  28. Andrew Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186(2), 2003. URL: http://dx.doi.org/10.1016/S0890-5401(03)00138-X.
  29. Vaughan Pratt. Modelling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33-71, 1986. URL: http://dx.doi.org/10.1007/BF01379149.
  30. Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In TLCA'97, volume 1210 of LNCS, pages 300-318. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-62688-3_43.
  31. Luca Roversi. A deep inference system with a self-dual binder which is complete for linear lambda calculus. J. of Log. and Comp., 26(2):677-698, 2016. URL: http://dx.doi.org/10.1093/logcom/exu033.
  32. Davide Sangiorgi. π-calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(1):235-274, 1996. URL: http://dx.doi.org/10.1016/0304-3975(96)00075-8.
  33. Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. Models for concurrency: towards a classification. Th. Comp. Sci., 170(1-2):297-348, 1996. URL: http://dx.doi.org/10.1016/S0304-3975(96)80710-9.
  34. Lutz Straßburger. Linear logic and noncommutativity in the calculus of structures. PhD thesis, TU Dresden, 2003. Google Scholar
  35. Lutz Straßburger. Some observations on the proof theory of second order propositional multiplicative linear logic. In TLCA 2009, volume 5608 of LNCS, pages 309-324. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_23.
  36. Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: the exponentials and decomposition. TOCL, 12(4):23, 2011. URL: http://dx.doi.org/10.1145/1970398.1970399.
  37. Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2:4):1-24, 2006. URL: http://dx.doi.org/10.2168/LMCS-2(2:4)2006.
  38. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. TOCL, 11(2):13, 2010. URL: http://dx.doi.org/10.1145/1656242.1656248.
  39. Rob van Glabbeek. The linear time-branching time spectrum (extended abstract). In CONCUR '90, volume 458 of LNCS, pages 278-297. Springer, 1990. URL: http://dx.doi.org/10.1007/BFb0039066.
  40. Rob van Glabbeek. Structure preserving bisimilarity, supporting an operational Petri net semantics of CCSP. In Correct System Design, volume 9360 of LNCS, pages 99-130. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23506-6_9.
  41. Rob van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4-5):229-327, 2001. URL: http://dx.doi.org/10.1007/s002360000041.
  42. Philip Wadler. Propositions as sessions. J. of Fun. Prog., 24(2-3):384-418, 2014. URL: http://dx.doi.org/10.1145/2364527.2364568.
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