2026-08-17T12:48:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6175 2024-03-06T10:38:30Z ddc:004 open_access

Private Names in Non-Commutative Logic Horne, Ross Tiu, Alwen Aman, Bogdan Ciobanu, Gabriel process calculi calculus of structures nominal logic causal consistency 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ross Horne and Alwen Tiu and Bogdan Aman and Gabriel Ciobanu 2016 Is Part Of LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2016.31 urn:nbn:de:0030-drops-61759 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.31 eng https://creativecommons.org/licenses/by/3.0/legalcode