{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:05:05Z","timestamp":1725541505158},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642106712"},{"type":"electronic","value":"9783642106729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10672-9_18","type":"book-chapter","created":{"date-parts":[[2009,12,2]],"date-time":"2009-12-02T09:08:11Z","timestamp":1259744891000},"page":"243-258","source":"Crossref","is-referenced-by-count":0,"title":["Classical Natural Deduction for S4 Modal Logic"],"prefix":"10.1007","author":[{"given":"Daisuke","family":"Kimura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoshihiko","family":"Kakutani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M., de Paiva, V.: On an intuitionistic modal logic. Studia Logica\u00a065(3), 383\u2013416 (2000)","journal-title":"Studia Logica"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. In: Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming, ICFP, pp. 233\u2013243 (2000)","DOI":"10.1145\/351240.351262"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1109\/LICS.1996.561317","volume-title":"Proceedings of 11 th Annual IEEE Symposium on Logic in Computer Science","author":"R. Davies","year":"1996","unstructured":"Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of 11 th Annual IEEE Symposium on Logic in Computer Science, pp. 184\u2013195. IEEE Computer Society Press, Los Alamitos (1996)"},{"issue":"3","key":"18_CR4","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM\u00a048(3), 555\u2013604 (2001)","journal-title":"Journal of the ACM"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","volume-title":"Logic Programming and Automated Reasoning","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: On the relation between the lambda-mu-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 31\u201343. Springer, Heidelberg (1994)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1007\/BFb0055098","volume-title":"Automata, Languages and Programming","author":"N. Ghani","year":"1998","unstructured":"Ghani, N., de Paiva, V., Ritter, E.: Explicit Substitutions for Constructive Necessity. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 743\u2013754. Springer, Heidelberg (1998)"},{"key":"18_CR7","first-page":"47","volume-title":"Proc. of the 1990 Principles of Programming Languages Conference","author":"T.G. Griffin","year":"1990","unstructured":"Griffin, T.G.: A formulae-as-types notion of control. In: Proc. of the 1990 Principles of Programming Languages Conference, pp. 47\u201358. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"6","key":"18_CR8","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1017\/S0960129598002667","volume":"8","author":"P.D. Groote","year":"1998","unstructured":"Groote, P.D.: An environment machine for the \u03bb\u03bc-calculus. Mathematical Structures in Computer Science\u00a08(6), 637\u2013669 (1998)","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/3-540-45793-3_34","volume-title":"Computer Science Logic","author":"Y. Kakutani","year":"2002","unstructured":"Kakutani, Y.: Duality between Call-by-Name Recursion and Call-by-Value Iteration. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol.\u00a02471, pp. 506\u2013521. Springer, Heidelberg (2002)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-76637-7_27","volume-title":"Programming Languages and Systems","author":"Y. Kakutani","year":"2007","unstructured":"Kakutani, Y.: Call-by-Name and Call-by-Value in Normal Modal Logic. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 399\u2013414. Springer, Heidelberg (2007)"},{"issue":"4","key":"18_CR11","first-page":"1721","volume":"48","author":"D. Kimura","year":"2007","unstructured":"Kimura, D.: Duality between Call-by-value Reductions and Call-by-name Reductions. IPSJ Journal\u00a048(4), 1721\u20131757 (2007)","journal-title":"IPSJ Journal"},{"issue":"3","key":"18_CR12","doi-asserted-by":"publisher","first-page":"799","DOI":"10.2178\/jsl\/1154698578","volume":"71","author":"M. Paz de","year":"2006","unstructured":"de Paz, M., Medeiros, N.: A new S4 classical modal logic in natural deduction. Journal of Symbolic Logic\u00a071(3), 799\u2013809 (2006)","journal-title":"Journal of Symbolic Logic"},{"key":"18_CR13","unstructured":"Nanevski, A.: A Modal Calculus for Exception Handling. In: The 3rd intuitionistic modal logics and applications workshop (2005)"},{"issue":"2","key":"18_CR14","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"Newman, M.H.A.: On theories with a combinatorial definition of \u201cequivalence\u201d. Annals of Mathematics\u00a043(2), 223\u2013243 (1942)","journal-title":"Annals of Mathematics"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Proc. of the Symposium on Principles of Programming Languages, pp. 215\u2013227 (1997)","DOI":"10.1145\/263699.263722"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Parigot, M.: Strong normalization for second order classical natural deduction. In: Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 39\u201346 (1993)","DOI":"10.1109\/LICS.1993.287602"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science\u00a011, 511\u2013540 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR19","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist and Wiksell, Stockholm (1965)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Selinger, P.: Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Mathematical Structures in Computer Science, 207\u2013260 (2001)","DOI":"10.1017\/S096012950000311X"},{"key":"18_CR21","unstructured":"Shan, C.-C.: A Computational Interpretation of Classical S4 Modal Logic. In: The 3rd intuitionistic modal logics and applications workshop (2005)"},{"issue":"1-2","key":"18_CR22","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(00)00053-0","volume":"248","author":"W. Taha","year":"2000","unstructured":"Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science\u00a0248(1-2), 211\u2013242 (2000)","journal-title":"Theoretical Computer Science"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/978-3-540-32033-3_15","volume-title":"Term Rewriting and Applications","author":"P. Wadler","year":"2005","unstructured":"Wadler, P.: Call-by-Value is Dual to Call-by-Name \u2013 Reloaded. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 185\u2013203. Springer, Heidelberg (2005)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 201\u2013212 (2006)","DOI":"10.1145\/1140335.1140360"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10672-9_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:37:56Z","timestamp":1619782676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10672-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642106712","9783642106729"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10672-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}