Private names in non-commutative logic

Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

3 Citations (Scopus)
7 Downloads (Pure)


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.
Original languageEnglish
Title of host publication27th International Conference on Concurrency Theory (CONCUR 2016)
EditorsJosée Desharnais, Radha Jagadeesan
Place of PublicationSaarbrücken/Wadern
Number of pages16
Publication statusPublished - 24 Aug 2016

Publication series

NameLeibniz International Proceedings in Informatics
ISSN (Print)1868-8969


  • process calculi
  • calculus of structures
  • nominal logic
  • causal consistency


Dive into the research topics of 'Private names in non-commutative logic'. Together they form a unique fingerprint.

Cite this