{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T20:26:59Z","timestamp":1648844819954},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,5,26]],"date-time":"2015-05-26T00:00:00Z","timestamp":1432598400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1007\/s11225-015-9616-1","type":"journal-article","created":{"date-parts":[[2015,5,25]],"date-time":"2015-05-25T06:48:27Z","timestamp":1432536507000},"page":"1225-1244","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reduction Rules for Intuitionistic $${{\\lambda}{\\rho}}$$ \u03bb \u03c1 -calculus"],"prefix":"10.1007","volume":"103","author":[{"given":"Ken-etsu","family":"Fujita","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryo","family":"Kashima","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuichi","family":"Komori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naosuke","family":"Matsuda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,26]]},"reference":[{"key":"9616_CR1","unstructured":"Andou, Y., A system of $${{\\lambda}{\\mu}}$$ \u03bb \u03bc -calculus proper to the implicational fragment of classical natural deduction with one conclusion, in RIMS Kokyuroku 976, 1997."},{"key":"9616_CR2","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.entcs.2004.06.029","volume":"117","author":"H. F. Cirstea","year":"2005","unstructured":"Cirstea H. F., Germain K. C.: A $${{\\rho}}$$ \u03c1 -calculus of explicit constraint application, Electronic Notes in Theoretical Computer Science 117, 51\u201367 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9616_CR3","doi-asserted-by":"crossref","unstructured":"Griffin, T. G., A formulae-as-type notion of control, in Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages 1989, 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"9616_CR4","doi-asserted-by":"crossref","unstructured":"Hindley, J. R., and J. P. Seldin, Lambda-Calculus and Combinators: An Introduction, Cambridge University Press, Cambridge, 2008.","DOI":"10.1017\/CBO9780511809835"},{"key":"9616_CR5","unstructured":"Howard, W. A., The formulae-as-types notion of construction, in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism 1980, 479\u2013490."},{"key":"9616_CR6","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0304-3975(96)00169-7","volume":"175","author":"S. Kobayashi","year":"1997","unstructured":"Kobayashi S.: Monad as modality, Theoretical Computer Science 175, 29\u201374 (1997)","journal-title":"Theoretical Computer Science"},{"key":"9616_CR7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s11225-013-9470-y","volume":"102","author":"Y. Komori","year":"2014","unstructured":"Komori Y., Matsuda N., Yamakawa F.: A Simplified Proof of the Church\u2013Rosser Theorem, Studia Logica 102, 175\u2013183 (2014)","journal-title":"Studia Logica"},{"key":"9616_CR8","doi-asserted-by":"crossref","first-page":"307","DOI":"10.21099\/tkbjm\/1389972031","volume":"37","author":"Y. Komori","year":"2013","unstructured":"Komori Y.: $${{\\lambda}{\\rho}}$$ \u03bb \u03c1 -calculus II, Tsukuba Journal of Mathematics 37, 307\u2013320 (2013)","journal-title":"Tsukuba Journal of Mathematics"},{"key":"9616_CR9","unstructured":"Miyamoto, K., and A. Igarashi, A modal foundation for secure information flow, in Proceedings of the Workshop on Foundations of Computer Security 2004, 187\u2013203."},{"key":"9616_CR10","unstructured":"Matsuda, N., Intuitionistic fragment of the $${{\\lambda}{\\mu}}$$ \u03bb \u03bc -calculus, Technical Report, Tokyo Institute of Technology C-282, 2015."},{"key":"9616_CR11","unstructured":"Matsuda, N., Intuitionistic tree sequent calculus and intuitionistic lambda-rho-calculus, in Post-proceedings of the RIMS Workshop \u201cProof Theory, Computability Theory and Related Issues\u201d, to appear."},{"key":"9616_CR12","unstructured":"Nakano, H., A $${{\\rho}}$$ \u03c1 -calculus of explicit constraint application, Logic, Language and Computation 61\u201372, 1994."},{"key":"9616_CR13","unstructured":"Nakano, H., The non-deterministic catch and throw mechanism and its subject reduction property, in Proceedings of Logic, Language and Computation 1992, 82\u201389."},{"key":"9616_CR14","doi-asserted-by":"crossref","unstructured":"Parigot, M., $${{\\lambda}{\\mu}}$$ \u03bb \u03bc -calculus: an algorithmic interpretation of classical natural deduction, in Proceedings of Logic programming and automated reasoning 1992, 190\u2013201.","DOI":"10.1007\/BFb0013061"},{"key":"9616_CR15","volume-title":"Lectures on the Curry\u2013Howard Isomorphism","author":"M. H. S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen M. H., Urzyczyn P.: Lectures on the Curry\u2013Howard Isomorphism, Elsevier, Amsterdam, (2006)"},{"key":"9616_CR16","unstructured":"Szabo, M. E., The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969."},{"key":"9616_CR17","doi-asserted-by":"crossref","unstructured":"Yamagata, Y., Strong normalization of second order symmetric lambda-mu calculus, Theoretical Aspects of Computer Software 459\u2013467, 2001.","DOI":"10.1007\/3-540-45500-0_23"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9616-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-015-9616-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9616-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,25]],"date-time":"2019-08-25T09:55:09Z","timestamp":1566726909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-015-9616-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,26]]},"references-count":17,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["9616"],"URL":"https:\/\/doi.org\/10.1007\/s11225-015-9616-1","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,26]]}}}