{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T08:22:18Z","timestamp":1648714938771},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4933,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,9]]},"abstract":"<jats:p>A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical <jats:italic>flow of information<\/jats:italic> inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as <jats:italic>deadlock free<\/jats:italic> Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the <jats:italic>causal dependencies<\/jats:italic> among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.<\/jats:p>","DOI":"10.1017\/s0960129500000797","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:13Z","timestamp":1236157273000},"page":"351-380","source":"Crossref","is-referenced-by-count":6,"title":["Causal dependencies in multiplicative linear logic with MIX"],"prefix":"10.1017","volume":"5","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000797_ref001","unstructured":"Asperti A. (1991) A linguistic approach to deadlock. Rapport de Recherche du Laboratoire d'Informatique de l'Ecole Normale Sup\u00e9rieure de Paris, LIENS\u201391\u201315."},{"key":"S0960129500000797_ref020","unstructured":"Roorda D. (1991) Resource Logics: Proof-theoretical Investigations. Ph.D. Thesis, University of Amsterdam."},{"key":"#cr-split#-S0960129500000797_ref005.1","unstructured":"Bellin G. (1993) Proof Nets for Multiplicative and Additive Linear Logic. (Draft"},{"key":"#cr-split#-S0960129500000797_ref005.2","unstructured":"early version as Report LFCS-91-161, May 1991, Department of Computer Science, University of Edinburgh.)"},{"key":"S0960129500000797_ref007","unstructured":"Bellin G. and van de Wiele J. (1993) Proof Nets and Typed lambda Calculus. I. Empires and Kingdoms. (Draft)"},{"key":"S0960129500000797_ref004","unstructured":"Bellin G. (1990) Mechanizing Proof theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information. Ph.D Thesis, Report CST\u201380\u201391, Department of Computer Science, University of Edinburgh."},{"key":"S0960129500000797_ref017","unstructured":"Retor\u00e9 C. (1990) A First Move from non Commutative Linear Logic to True Concurrency: the calculus of ordered sequents. (Draft)"},{"key":"S0960129500000797_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69968-9"},{"key":"S0960129500000797_ref015","unstructured":"Petri C. A. (1962) Kommunication mit Automaten. Schriften des Institutes f\u00fcr Instruentelle Mathematik, Bonn."},{"key":"S0960129500000797_ref010","unstructured":"Fleury A. and Retor\u00e9 C. (1991) The MIX rule. (Draft)"},{"key":"S0960129500000797_ref019","unstructured":"Roorda D. (1990) Quantum Graphs and Proof Nets. (Draft)"},{"key":"S0960129500000797_ref002","doi-asserted-by":"crossref","unstructured":"Asperti A. , Ferrari G. and Gorrieri R. (1990) Implicative Formulae in the 'Proofs-as-Computations analogy. Proc. of the 17th Symposium on Principles of Programming Languages (POPL 90), San Francisco.","DOI":"10.1145\/96709.96715"},{"key":"S0960129500000797_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90069-R"},{"key":"S0960129500000797_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01622878"},{"key":"S0960129500000797_ref011","unstructured":"Gallier J. (1991) Constructive Logics. Part II: Linear logic and Proof Nets. Technical Report of Digital Paris Research Laboratory 9."},{"key":"S0960129500000797_ref012","unstructured":"Girard J. Y. (1986) Linear Logic. Theoretical Computer Science 50."},{"key":"S0960129500000797_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90047-1"},{"key":"S0960129500000797_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018359"},{"key":"S0960129500000797_ref018","unstructured":"Retore C. (1993) R\u00e9seaux et S\u00e9quents Ordonn\u00e9s. Th\u00e9se de doctorat, Universit\u00e9 Paris VII."},{"key":"S0960129500000797_ref021","unstructured":"Troelstra A. S. (1990) Lectures on Linear logic. Techical Report X\u201390\u201315, University of Amsterdam."},{"key":"S0960129500000797_ref003","volume-title":"Categories. Types and Structures. An introduction to Category Theory for the working computer scientist","author":"Asperti","year":"1991"},{"key":"S0960129500000797_ref008","unstructured":"Danos V. (1990) La Logique Lin\u00e9aire appliqu\u00e9e \u00e0 l'\u00e9tude de divers processus de normalization. These de doctorat, Universit\u00e9 Paris VII."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T21:03:19Z","timestamp":1557781399000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000797\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["S0960129500000797"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000797","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}