{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:45:03Z","timestamp":1740123903599,"version":"3.37.3"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,9,14]],"date-time":"2018-09-14T00:00:00Z","timestamp":1536883200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,9,14]],"date-time":"2018-09-14T00:00:00Z","timestamp":1536883200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["KAKENHI (Grant-in-Aid for JSPS Fellows) 16J04925"],"award-info":[{"award-number":["KAKENHI (Grant-in-Aid for JSPS Fellows) 16J04925"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Philos Logic"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10992-018-9484-z","type":"journal-article","created":{"date-parts":[[2018,9,14]],"date-time":"2018-09-14T18:40:41Z","timestamp":1536950441000},"page":"553-570","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms"],"prefix":"10.1007","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5214-7077","authenticated-orcid":false,"given":"Yuta","family":"Takahashi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryo","family":"Takemura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,14]]},"reference":[{"unstructured":"Gallier, J. (1990). On Girard\u2019s Candidats de reductibilit\u00e9. In Odifreddi, P. (Ed.) Logic and computer science (pp. 123\u2013203). London: Academic Press.","key":"9484_CR1"},{"key":"9484_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50, 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"9484_CR3","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.tcs.2004.10.022","volume":"333","author":"J Laird","year":"2005","unstructured":"Laird, J. (2005). Game semantics and linear CPS translation. Theoretical Computer Science, 333, 199\u2013224.","journal-title":"Theoretical Computer Science"},{"key":"9484_CR4","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","volume":"281","author":"M Okada","year":"2002","unstructured":"Okada, M. (2002). A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science, 281, 471\u201398.","journal-title":"Theoretical Computer Science"},{"unstructured":"Okada, M., & Takemura, R. (2007). Remarks on semantic completeness for proof-terms with Lairds dual affine\/intuitionistic \u03bb-calculus. In Comon-Lundh, H., Kirchner, C., Kirchner, H. (Eds.) Rewriting, computation and proof: essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday. Volume 4600 of lecture notes in computer science (pp. 167\u201381). Berlin: Springer.","key":"9484_CR5"},{"doi-asserted-by":"crossref","unstructured":"Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J.E. (Ed.) Proceedings of the second scandinavian logic symposium, studies in logic and the foundations of mathematics, (Vol. 63, pp 235\u2013307. Amsterdam: North-Holland.","key":"9484_CR6","DOI":"10.1016\/S0049-237X(08)70849-8"},{"unstructured":"Prawitz, D. (1973). Towards a foundation of a general proof theory. In Suppes, P., Henkin, L., Joja, A., Moisil, GC (Eds.) Logic, methodology and philosophy of science IV (pp. 225\u2013250). Amsterdam: North-Holland.","key":"9484_CR7"},{"unstructured":"Riba, C. (2008). Toward a general rewriting-based framework for reducibility. <hal-00779623>.","key":"9484_CR8"},{"key":"9484_CR9","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","volume":"148","author":"P Schroeder-Heister","year":"2006","unstructured":"Schroeder-Heister, P. (2006). Validity concepts in proof-theoretic semantics. Synthese, 148, 525\u201371.","journal-title":"Synthese"},{"unstructured":"Schroeder-Heister, P. (2016). Proof-theoretic semantics. In Zalta, E.N. (Ed.) The Stanford Encyclopedia of Philosophy, Winter 2016 Edition. \n                    https:\/\/plato.stanford.edu\/archives\/win2016\/entries\/proof-theoretic-semantics\/\n                    \n                  .","key":"9484_CR10"},{"key":"9484_CR11","volume-title":"Lectures on the Curry-Howard isomorphism","author":"MH S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard isomorphism. Amsterdam: Elsevier."}],"container-title":["Journal of Philosophical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-018-9484-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10992-018-9484-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-018-9484-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:59:02Z","timestamp":1589414342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10992-018-9484-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,14]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["9484"],"URL":"https:\/\/doi.org\/10.1007\/s10992-018-9484-z","relation":{},"ISSN":["0022-3611","1573-0433"],"issn-type":[{"type":"print","value":"0022-3611"},{"type":"electronic","value":"1573-0433"}],"subject":[],"published":{"date-parts":[[2018,9,14]]},"assertion":[{"value":"14 August 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 September 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}