{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:47:35Z","timestamp":1656798455015},"reference-count":17,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3855,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s0304-3975(01)00177-3","type":"journal-article","created":{"date-parts":[[2003,1,30]],"date-time":"2003-01-30T14:22:41Z","timestamp":1043936561000},"page":"525-549","source":"Crossref","is-referenced-by-count":12,"title":["Phase semantics for light linear logic"],"prefix":"10.1016","volume":"294","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\/S0304-3975(01)00177-3_BIB1","first-page":"159","article-title":"The structure of exponentials: uncovering the dynamics of linear logic proofs","volume":"Vol. 713","author":"Danos","year":"1993"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB2","series-title":"Proc. 2nd Scandinavian Logic Symposium","first-page":"63","article-title":"Une extension de l'interpr\u00e9tation de G\u00f6del a l'analyse, et son application a l\u2019\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types","author":"Girard","year":"1971"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB4","volume":"Vol. 7","author":"Girard","year":"1988"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB5","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1006\/inco.1998.2700","article-title":"Light linear logic","volume":"14","author":"Girard","year":"1998","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB6","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":"Theoret. Comp. Sci."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB7","doi-asserted-by":"crossref","unstructured":"M.I. Kanovich, T. Ito, Temporal linear logic specifications for concurrent processes, in: Proc. 12th Ann. IEEE Symp. on Logic in Computer Science, Warsaw, Poland, 1997.","DOI":"10.1109\/LICS.1997.614928"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB8","doi-asserted-by":"crossref","unstructured":"M.I. Kanovich, M. Okada, A. Scedrov, Phase semantics for light linear logic: extended abstract, in: Proc. 13th Conf. on the Mathematical Foundations of Programming Semantics, Pittsburgh, Pennsylvania, USA, 1997, Electronic Notes in Theoretical Computer Science. http:\/\/www1.elsevier.nl\/mcs\/tcs\/pc\/Menu.html.","DOI":"10.1016\/S1571-0661(05)80159-8"},{"key":"10.1016\/S0304-3975(01)00177-3_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":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(01)00177-3_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":"Inform. Comput."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB11","first-page":"197","article-title":"On the fine structure of the exponential rule","volume":"Vol. 222","author":"Martini","year":"1995"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB12","doi-asserted-by":"crossref","unstructured":"M. Okada, Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract), in: J.-Y. Girard, M. Okada, A. Scedrov, (Eds.), ENTCS (Electronic Notes in Theoretical Computer Science), Vol. 3, A Special Issue on Linear Logic 96, Tokyo Meeting. ENTCS, Elsevier, Amsterdam 1996.","DOI":"10.1016\/S1571-0661(05)80414-1"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB13","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/S0304-3975(99)00058-4","article-title":"Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic","volume":"227","author":"Okada","year":"1999","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB14","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","article-title":"A uniform semantic proof for cut-elimination and completeness of various first and higher order logics","volume":"281","author":"Okada","year":"2002","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00177-3_BIB15","doi-asserted-by":"crossref","first-page":"790","DOI":"10.2307\/2586501","article-title":"The finite model property for various fragments of intuitionistic linear logic","volume":"64","author":"Okada","year":"1999","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB16","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, in: Proc. 18th Ann. Symp. on the Foundations of Computer Science, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S0304-3975(01)00177-3_BIB17","doi-asserted-by":"crossref","unstructured":"K. Terui, Light affine lambda calculus and polytime strong normalization, in: Proc. 16th Ann. IEEE Conference on Logic in Computer Science, 2001, pp. 209\u2013220.","DOI":"10.1109\/LICS.2001.932498"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001773?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001773?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T00:27:23Z","timestamp":1553905643000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501001773"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S0304397501001773"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00177-3","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}