{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T00:26:45Z","timestamp":1787531205521,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642220111","type":"print"},{"value":"9783642220128","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22012-8_13","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:29:39Z","timestamp":1308367779000},"page":"174-185","source":"Crossref","is-referenced-by-count":2,"title":["Relating Computational Effects by \u22a4\u2009\u22a4-Lifting"],"prefix":"10.1007","author":[{"given":"Shin-ya","family":"Katsumata","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-45699-6_2","volume-title":"Applied Semantics","author":"N. Benton","year":"2002","unstructured":"Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 42\u2013122. Springer, Heidelberg (2002)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Filinski, A.: Representing monads. In: Proc. POPL 1994, pp. 446\u2013457 (1994)","DOI":"10.1145\/174675.178047"},{"key":"13_CR3","unstructured":"Filinski, A.: Controlling Effects. PhD thesis, Carnegie Mellon University (1996)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Filinski, A.: Representing layered monads. In: Proc. POPL 1999, pp. 175\u2013188 (1999)","DOI":"10.1145\/292540.292557"},{"issue":"1-3","key":"13_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.tcs.2006.12.027","volume":"375","author":"A. Filinski","year":"2007","unstructured":"Filinski, A.: On the relations between monadic semantics. Theor. Comput. Sci.\u00a0375(1-3), 41\u201375 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1291151.1291168","volume-title":"ICFP","author":"A. Filinski","year":"2007","unstructured":"Filinski, A., St\u00f8vring, K.: Inductive reasoning about effectful data types. In: Hinze, R., Ramsey, N. (eds.) ICFP, pp. 97\u2013110. ACM, New York (2007)"},{"key":"13_CR7","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.: Linear logic. Theor. Comp. Sci.\u00a050, 1\u2013102 (1987)","journal-title":"Theor. Comp. Sci."},{"issue":"2-3","key":"13_CR8","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1020895213317","volume":"15","author":"M. Hasegawa","year":"2002","unstructured":"Hasegawa, M., Kakutani, Y.: Axioms for recursion in call-by-value. Higher-Order and Symbolic Computation\u00a015(2-3), 235\u2013264 (2002)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Hermida, C.: Fibrations, Logical Predicates and Indeterminants. PhD thesis, University of Edinburgh (1993)","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"13_CR10","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11538363_8","volume-title":"Computer Science Logic","author":"S. Katsumata","year":"2005","unstructured":"Katsumata, S.: A semantic formulation of \u22a4\u2009\u22a4-lifting and logical predicates for computational metalanguage. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 87\u2013102. Springer, Heidelberg (2005)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-87531-4_21","volume-title":"Computer Science Logic","author":"S. Katsumata","year":"2008","unstructured":"Katsumata, S.: A characterisation of lambda definability with sums via \u22a4\u2009\u22a4-closure operators. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 278\u2013292. Springer, Heidelberg (2008)"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1017\/S0960129508007172","volume":"18","author":"J.-G. Larrecq","year":"2008","unstructured":"Larrecq, J.-G., Lasota, S., Nowak, D.: Logical relations for monadic types. Math. Struct. in Comp. Science\u00a018, 1169\u20131217 (2008)","journal-title":"Math. Struct. in Comp. Science"},{"key":"13_CR14","unstructured":"Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2004)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11417170_20","volume-title":"Typed Lambda Calculi and Applications","author":"S. Lindley","year":"2005","unstructured":"Lindley, S., Stark, I.: Reducibility and \u22a4\u2009\u22a4-lifting for computation types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 262\u2013277. Springer, Heidelberg (2005)"},{"key":"13_CR16","first-page":"82","volume-title":"LICS","author":"P.-A. Melli\u00e8s","year":"2005","unstructured":"Melli\u00e8s, P.-A., Vouillon, J.: Recursive polymorphic types and parametricity in an operational framework. In: LICS, pp. 82\u201391. IEEE Computer Society, Los Alamitos (2005)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Mitchell, J.: Representation independence and data abstraction. In: Proc. POPL 1986, pp. 263\u2013276 (1986)","DOI":"10.1145\/512644.512669"},{"key":"13_CR18","volume-title":"Foundations for Programming Languages","author":"J. Mitchell","year":"1996","unstructured":"Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-56992-8_21","volume-title":"Computer Science Logic","author":"J. Mitchell","year":"1993","unstructured":"Mitchell, J., Scedrov, A.: Notes on sconing and relators. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 352\u2013378. Springer, Heidelberg (1993)"},{"issue":"4","key":"13_CR20","doi-asserted-by":"publisher","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic\u00a062(4), 1461\u20131479 (1997)","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"13_CR21","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1017\/S0960129500003066","volume":"10","author":"A. Pitts","year":"2000","unstructured":"Pitts, A.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science\u00a010(3), 321\u2013359 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Semantics for algebraic operations. Electr. Notes Theor. Comput. Sci.\u00a045 (2001)","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-00590-9_7","volume-title":"Programming Languages and Systems","author":"G.D. Plotkin","year":"2009","unstructured":"Plotkin, G.D., Pretnar, M.: Handlers of algebraic effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 80\u201394. Springer, Heidelberg (2009)"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Simpson, A., Plotkin, G.: Complete axioms for categorical fixed-point operators. In: LICS, pp. 30\u201341 (2000)","DOI":"10.1109\/LICS.2000.855753"},{"issue":"1","key":"13_CR25","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01806033","volume":"9","author":"I. Stark","year":"1996","unstructured":"Stark, I.: Categorical models for local names. Lisp and Symbolic Computation\u00a09(1), 77\u2013107 (1996)","journal-title":"Lisp and Symbolic Computation"},{"key":"13_CR26","first-page":"36","volume-title":"Proc. LICS 1996","author":"I. Stark","year":"1996","unstructured":"Stark, I.: A fully abstract domain model for the \u03c0-calculus. In: Proc. LICS 1996, pp. 36\u201342. IEEE, Los Alamitos (1996)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22012-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:06:53Z","timestamp":1560283613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22012-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642220111","9783642220128"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22012-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}