2 Search Results for "Ciobanu, Gabriel"


Document
The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic

Authors: Ross Horne

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
Probabilistic choice, where each branch of a choice is weighted according to a probability distribution, is an established approach for modelling processes, quantifying uncertainty in the environment and other sources of randomness. This paper uncovers new insight showing probabilistic choice has a purely logical interpretation as an operator in an extension of linear logic. By forbidding projection and injection, we reveal additive operators between the standard with and plus operators of linear logic. We call these operators the sub-additives. The attention of the reader is drawn to two sub-additive operators: the first being sound with respect to probabilistic choice; while the second arises due to the fact that probabilistic choice cannot be self-dual, hence has a de Morgan dual counterpart. The proof theoretic justification for the sub-additives is a cut elimination result, employing a technique called decomposition. The justification from the perspective of modelling probabilistic concurrent processes is that implication is sound with respect to established notions of probabilistic refinement, and is fully compositional.

Cite as

Ross Horne. The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{horne:LIPIcs.FSCD.2019.23,
  author =	{Horne, Ross},
  title =	{{The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.23},
  URN =		{urn:nbn:de:0030-drops-105300},
  doi =		{10.4230/LIPIcs.FSCD.2019.23},
  annote =	{Keywords: calculus of structures, probabilistic choice, probabilistic refinement}
}
Document
Private Names in Non-Commutative Logic

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

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{horne_et_al:LIPIcs.CONCUR.2016.31,
  author =	{Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel},
  title =	{{Private Names in Non-Commutative Logic}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.31},
  URN =		{urn:nbn:de:0030-drops-61759},
  doi =		{10.4230/LIPIcs.CONCUR.2016.31},
  annote =	{Keywords: process calculi, calculus of structures, nominal logic, causal consistency}
}
  • Refine by Author
  • 2 Horne, Ross
  • 1 Aman, Bogdan
  • 1 Ciobanu, Gabriel
  • 1 Tiu, Alwen

  • Refine by Classification
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Process calculi
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 2 calculus of structures
  • 1 causal consistency
  • 1 nominal logic
  • 1 probabilistic choice
  • 1 probabilistic refinement
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2016
  • 1 2019

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