{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:01Z","timestamp":1761610321464,"version":"build-2065373602"},"reference-count":12,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2005,5,24]],"date-time":"2005-05-24T00:00:00Z","timestamp":1116892800000},"content-version":"vor","delay-in-days":3065,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1997]]},"DOI":"10.1016\/s1571-0661(05)80159-8","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"221-234","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":7,"special_numbering":"C","title":["Phase Semantics for Light Linear Logic (Extended Abstract)"],"prefix":"10.1016","volume":"6","author":[{"given":"Max I.","family":"Kanovich","sequence":"first","affiliation":[]},{"given":"Mitsuhiro","family":"Okada","sequence":"additional","affiliation":[]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80159-8_BIB1","article-title":"Light linear logic","author":"Jean-Yves Girard","year":"1995","journal-title":"Manuscript"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB2","series-title":"Cambridge Tracts in Theoretical Computer Science 7","article-title":"Proofs and Types","author":"Jean-Yves","year":"1988"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Jean-Yves","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","article-title":"Bounded linear logic: A modular approach to polynomial time computability","volume":"97","author":"Girard","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB5","doi-asserted-by":"crossref","unstructured":"Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings of the Third Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory, pages 159\u2013171. Springer-Verlag LNCS 713, 1993.","DOI":"10.1007\/BFb0022564"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB6","first-page":"197","article-title":"On the fine structure of the exponential rule","volume":"Vol. 222","author":"Martini","year":"1995"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB7","unstructured":"Max I. Kanovich and Takayasu Ito. Temporal linear logic specifications for concurrent processes. In Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 1997."},{"key":"10.1016\/S1571-0661(05)80159-8_BIB8","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The temporal logic of programs. In Proc. 18-th Annual Symposium on the Foundations of Computer Science, pages 46\u201357. 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB9","doi-asserted-by":"crossref","first-page":"541","DOI":"10.2307\/2275674","article-title":"The undecidability of second order linear logic without exponentials","volume":"61","author":"Lafont","year":"1996","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB10","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1006\/inco.1996.0019","article-title":"The undecidability of second order multiplicative linear logic","volume":"125","author":"Lafont","year":"1996","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB11","doi-asserted-by":"crossref","unstructured":"Mitsuhiro Okada. Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract). In J.-Y. Girard, M. Okada, and A. Scedrov, editors, ENTCS (Electronic Notes in Theoretical Computer Science) Vol.3: A Special Issue on Linear Logic 96, Tokyo Meeting. URL: http:\/\/www.elsevier.nl\/locate\/entcs\/volume3.html, 1996. Pull version submitted to Theoretical Computer Science, also available by anonymous ftp at http:\/\/abelard.flet.mita.keio.ac.jp\/person\/mitsu\/paper.html or ftp:\/\/abelard.flet.mita.keio.ac.jp\/pub\/Papers\/mitsu.","DOI":"10.1016\/S1571-0661(05)80414-1"},{"key":"10.1016\/S1571-0661(05)80159-8_BIB12","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. Une extension de l'interpretation de G\u00f6del a l'analyse, et son application a l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In J.P. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63\u201392. North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801598?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801598?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:07:08Z","timestamp":1761610028000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105801598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"references-count":12,"alternative-id":["S1571066105801598"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80159-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Phase Semantics for Light Linear Logic (Extended Abstract)","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80159-8","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1997 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}