{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T10:52:08Z","timestamp":1672483928525},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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":[[2016,6]]},"abstract":"<jats:p>We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of barbed preorder for a CCS-like process calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely simulation and labelled transition systems. This result establishes a connection between an approach to reason about process specifications, the barbed preorder, and a method to reason about logic specifications, the logical preorder.<\/jats:p>","DOI":"10.1017\/s0960129514000413","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T12:05:14Z","timestamp":1415621114000},"page":"868-906","source":"Crossref","is-referenced-by-count":2,"title":["Relating reasoning methodologies in linear logic and process algebra"],"prefix":"10.1017","volume":"26","author":[{"given":"YUXIN","family":"DENG","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ROBERT J.","family":"SIMMONS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ILIANO","family":"CERVESATO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129514000413_ref23","unstructured":"Lincoln P. and Saraswat V. (1991) Proofs as concurrent processes: A logical interpretation for concurrent constraint programming. Technical report, Systems Sciences Laboratory, Xerox PARC."},{"key":"S0960129514000413_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00074-7"},{"key":"S0960129514000413_ref10","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.6.939"},{"key":"S0960129514000413_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.11.006"},{"key":"S0960129514000413_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00223-5"},{"key":"S0960129514000413_ref7","volume-title":"Workshop on Formal Methods and Computer Security \u2013 FMCS'00","author":"Cervesato","year":"2000"},{"key":"S0960129514000413_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_36"},{"key":"S0960129514000413_ref3","unstructured":"Barber A. (1996) Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Sciences, University of Edinburgh."},{"key":"S0960129514000413_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0960129514000413_ref6","first-page":"1","volume-title":"Proceedings of the Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation","author":"Caires","year":"2012"},{"key":"S0960129514000413_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.006"},{"key":"S0960129514000413_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00137-8"},{"key":"S0960129514000413_ref31","volume-title":"The \u03c0-Calculus: A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S0960129514000413_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129514000413_ref28","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2832"},{"key":"S0960129514000413_ref8","unstructured":"Cervesato I. , Pfenning F. , Walker D. and Watkins K. (2002) A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-2002-002, Department of Computer Science, Carnegie Mellon University. Revised May 2003."},{"key":"S0960129514000413_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129514000413_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_24"},{"key":"S0960129514000413_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00168-2"},{"key":"S0960129514000413_ref19","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129514000413_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.005"},{"key":"S0960129514000413_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00103-0"},{"key":"S0960129514000413_ref21","volume-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"S0960129514000413_ref11","unstructured":"Deng Y. and Du W. (2011) Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical Report CMU-CS-11-110, Carnegie Mellon University."},{"key":"S0960129514000413_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56454-3_13"},{"key":"S0960129514000413_ref27","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S0960129514000413_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.01.006"},{"key":"S0960129514000413_ref24","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws.","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"S0960129514000413_ref33","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/2364527.2364568","volume-title":"Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming","author":"Wadler","year":"2012"},{"key":"S0960129514000413_ref15","unstructured":"Fournet C. and Gonthier G. (2000) The join calculus: A language for distributed mobile programming. Applied Semantics Summer School \u2013 APPSEM'00, Caminha. Available at http:\/\/research.microsoft.com\/~fournet."},{"key":"S0960129514000413_ref13","first-page":"313","volume-title":"Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science","author":"Deng","year":"2007"},{"key":"S0960129514000413_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"S0960129514000413_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000413","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T21:54:28Z","timestamp":1650578068000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000413\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["S0960129514000413"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000413","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}