{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T10:44:02Z","timestamp":1648637042862},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2007,4,1]],"date-time":"2007-04-01T00:00:00Z","timestamp":1175385600000},"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":[[2007,4]]},"abstract":"<jats:p>We study full completeness and syntactical separability of <jats:italic>MLL<\/jats:italic> proof nets with the mix rule. The general method we use consists of first addressing these two questions in the less restrictive framework of proof structures, and then adapting the results to proof nets.<\/jats:p><jats:p>At the level of proof structures, we find a semantical characterisation of their interpretations in relational semantics, and define an observational equivalence that is proved to be the equivalence induced by cut elimination. Hence, we obtain a semantical characterisation (in coherent spaces) and an observational equivalence for the proof nets with the mix rule.<\/jats:p>","DOI":"10.1017\/s0960129506005652","type":"journal-article","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:02:05Z","timestamp":1178211725000},"page":"341-359","source":"Crossref","is-referenced-by-count":5,"title":["Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic"],"prefix":"10.1017","volume":"17","author":[{"given":"MICHELE","family":"PAGANI","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,4,1]]},"reference":[{"key":"S0960129506005652_N101A9","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"S0960129506005652_N1028C","unstructured":"Morris J. H. (1968) \u03bb-calculus models of programming languages, Ph.D. thesis, MIT."},{"key":"S0960129506005652_N102E2","unstructured":"Tan A. (1997) Full completeness for models of linear logic, Ph.D. thesis, University of Oxford."},{"key":"S0960129506005652_N10166","doi-asserted-by":"publisher","DOI":"10.2307\/2694930"},{"key":"S0960129506005652_N10104","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.05.002"},{"key":"S0960129506005652_N102F4","unstructured":"Tortora de Falco L. (2000) R\u00e9seaux, coh\u00e9rence et exp\u00e9riences obsessionnelles. Th\u00e8se de doctorat, Universit\u00e9 Paris VII. (Available at: http:\/\/www.logique.jussieu.fr\/www.tortora\/index.html.)"},{"key":"S0960129506005652_N102D0","unstructured":"Statman R. (1983) Completeness, invariance and \u03bb-definability. Journal of Symbolic Logic 17\u201326."},{"key":"S0960129506005652_N10254","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90263-1"},{"key":"S0960129506005652_N10222","unstructured":"Joly T. (2000) Codages, s\u00e9parabilit\u00e9 et repr\u00e9sentation de fonctions en \u03bb-calcul simplement typ\u00e9 et dans d'autres syst\u00e8mes de types, Th\u00e8se de doctorat, Universit\u00e9 Paris VII."},{"key":"S0960129506005652_N1020A","unstructured":"Hughes D. and van Glabbeek R. (2003) Proof nets for unit-free multiplicative-additive linear logic. In: Proceedings of the eighteenth annual symposium on Logic In Computer Science, IEEE Computer Society Press 1\u201310."},{"key":"S0960129506005652_N10234","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00297-3"},{"key":"S0960129506005652_N1030A","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503003967"},{"key":"S0960129506005652_N100C2","doi-asserted-by":"publisher","DOI":"10.2307\/2275407"},{"key":"S0960129506005652_N1018C","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129506005652_N100E8","unstructured":"Bellin G. and de Wiele J. V. (1995) Subnets of proof-nets in MLL. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series 222, Cambridge University Press."},{"key":"S0960129506005652_N1012D","first-page":"1","article-title":"Alcune propriet\u00e0 delle forme \u03b2 \u03b7-normali nel \u03bb-K-calcolo","volume":"696","year":"1968","journal-title":"Pubblicazioni dell'IAC"},{"key":"S0960129506005652_N10143","doi-asserted-by":"publisher","DOI":"10.1007\/BF01622878"},{"key":"S0960129506005652_N1029E","unstructured":"Pagani M. (2006) Proof nets and cliques: towards the understanding of analytical proofs, Ph.D. thesis, Universit\u00e0 Roma Tre and Universit\u00e9 Aix-Marseille II."},{"key":"S0960129506005652_N1027A","unstructured":"Matsuoka S. (2005) Weak typed B\u00f6hm theorem on IMLL (submitted for publication). (Available at: http:\/\/arxiv.org\/abs\/cs.LO\/0410030.)"},{"key":"S0960129506005652_N102B0","doi-asserted-by":"publisher","DOI":"10.1017\/S096012959700234X"},{"key":"S0960129506005652_N101C9","volume-title":"Logic and Algebra","author":"Girard","year":"1996"},{"key":"S0960129506005652_N101EA","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129506005652","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T20:24:10Z","timestamp":1554755050000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129506005652\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,4]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,4]]}},"alternative-id":["S0960129506005652"],"URL":"https:\/\/doi.org\/10.1017\/s0960129506005652","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,4]]}}}