{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:07Z","timestamp":1747173427789,"version":"3.40.5"},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T00:00:00Z","timestamp":1553817600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of <jats:italic>\u03c0<\/jats:italic>-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the <jats:italic>\u03c0<\/jats:italic> -calculus is established. A novel contribution of this work is that we generalise the notion of a \u2018left proof\u2019 to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal <jats:italic>\u03c0<\/jats:italic> -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.<\/jats:p>","DOI":"10.1017\/s0960129518000452","type":"journal-article","created":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T05:47:23Z","timestamp":1553838443000},"page":"1275-1308","source":"Crossref","is-referenced-by-count":1,"title":["Constructing weak simulations from linear implications for processes with private names"],"prefix":"10.1017","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0162-1901","authenticated-orcid":false,"given":"Ross","family":"Horne","sequence":"first","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2019,3,29]]},"reference":[{"key":"S0960129518000452_ref23","unstructured":"Horne, R. , Tiu, A. , Aman, B. and Ciobanu, G. (2018). Polarised Nominal Quantifiers Model Private Names in Non-commutative Logic. Technical Report 1502. ISSN 1842-1490, extended version of above supporting submission to TOCL. http:\/\/iit.iit.tuiasi.ro\/TR\/reports\/fml1502.pdf."},{"key":"S0960129518000452_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182614"},{"key":"S0960129518000452_ref2","volume-title":"28th International Conference on Concurrency Theory (CONCUR 2017)","volume":"85","author":"Ahn","year":"2017"},{"key":"S0960129518000452_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_24"},{"key":"S0960129518000452_ref22","volume-title":"27th International Conference on Concurrency Theory (CONCUR 2016)","volume":"59","author":"Horne","year":"2016"},{"key":"S0960129518000452_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"S0960129518000452_ref12","first-page":"313","volume-title":"22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007","author":"Deng","year":"2007"},{"key":"S0960129518000452_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_13"},{"key":"S0960129518000452_ref6","first-page":"61","volume-title":"International Conference on Concurrency Theory","volume":"8052","author":"Bernardi","year":"2013"},{"key":"S0960129518000452_ref39","first-page":"278","volume-title":"CONCUR 1990, Amsterdam, The Netherlands, August 27\u201330","volume":"458","author":"van Glabbeek","year":"1990"},{"key":"S0960129518000452_ref32","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu033"},{"key":"S0960129518000452_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0960129518000452_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S0960129518000452_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951100003X"},{"key":"S0960129518000452_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"S0960129518000452_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"S0960129518000452_ref11","first-page":"91","volume-title":"Perspectives of System Informatics","author":"Ciobanu","year":"2015"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner","key":"S0960129518000452_ref28"},{"key":"S0960129518000452_ref5","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"S0960129518000452_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00103-0"},{"key":"S0960129518000452_ref3","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129518000452_ref8","first-page":"302","volume-title":"Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29\u2013August 1, Proceedings","volume":"2401","author":"Bruscoli","year":"2002"},{"key":"S0960129518000452_ref10","first-page":"159","volume-title":"Computer Science Logic (CSL 2011) - 25th International Workshop\/20th Annual Conference of the EACSL","volume":"12","author":"Chaudhuri","year":"2011"},{"key":"S0960129518000452_ref13","first-page":"174","volume-title":"Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8\u201312","author":"Deni\u00e9lou","year":"2013"},{"key":"S0960129518000452_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"S0960129518000452_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129518000452_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"S0960129518000452_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_5"},{"key":"S0960129518000452_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S0960129518000452_ref21","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1531"},{"key":"S0960129518000452_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00168-2"},{"key":"S0960129518000452_ref25","first-page":"242","volume-title":"Extensions of Logic Programming, Third International Workshop, ELP 1992, Bologna, Italy, February 26\u201328, 1992, Proceedings","volume":"660","author":"Miller","year":"1993"},{"key":"S0960129518000452_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S0960129518000452_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"S0960129518000452_ref20","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2015.2.245"},{"key":"S0960129518000452_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62688-3_43"},{"key":"S0960129518000452_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050036"},{"key":"S0960129518000452_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)80710-9"},{"key":"S0960129518000452_ref36","first-page":"23","article-title":"A system of interaction and structure IV: the exponentials and decomposition","volume":"12","author":"Stra\u00dfburger","year":"2011","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"S0960129518000452_ref37","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(2:4)2006"},{"key":"S0960129518000452_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s002360000041"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T10:24:59Z","timestamp":1570530299000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000452\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,29]]},"references-count":41,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129518000452"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000452","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2019,3,29]]}}}