{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:51:51Z","timestamp":1760079111171},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540282310"},{"type":"electronic","value":"9783540318972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_8","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:35:33Z","timestamp":1127828133000},"page":"87-102","source":"Crossref","is-referenced-by-count":15,"title":["A Semantic Formulation of \u22a4\u2009\u22a4-Lifting and Logical Predicates for Computational Metalanguage"],"prefix":"10.1007","author":[{"given":"Shin-ya","family":"Katsumata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","first-page":"313","volume":"10","author":"M. Abadi","year":"2000","unstructured":"Abadi, M.: TT-closed relations and admissibility. MSCS\u00a010(3), 313\u2013320 (2000)","journal-title":"MSCS"},{"key":"8_CR2","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511983504","volume-title":"Domains and Lambda-Calculi","author":"R. Amadio","year":"1998","unstructured":"Amadio, R., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, vol.\u00a046. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-45793-3_37","volume-title":"Computer Science Logic","author":"J. G.-Larrecq","year":"2002","unstructured":"G.-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 553\u2013568. Springer, Heidelberg (2002)"},{"key":"8_CR4","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."},{"key":"8_CR5","unstructured":"Hasegawa, M.: Categorical glueing and logical predicates for models of linear logic. Technical Report RIMS-1223, Research Institute for Mathematical Sciences, Kyoto University (1999)"},{"key":"8_CR6","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":"8_CR7","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1017\/S0956796802004409","volume":"13","author":"P. Johann","year":"2003","unstructured":"Johann, P.: Short cut fusion is correct. J. Funct. Program.\u00a013(4), 797\u2013814 (2003)","journal-title":"J. Funct. Program."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BFb0037110","volume-title":"Typed Lambda Calculi and Applications","author":"A. Jung","year":"1993","unstructured":"Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 245\u2013257. Springer, Heidelberg (1993)"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BF01304852","volume":"23","author":"A. Kock","year":"1970","unstructured":"Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik\u00a023, 113\u2013120 (1970)","journal-title":"Archiv der Mathematik"},{"key":"8_CR11","unstructured":"Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2004)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Lindley, S., Stark, I.: Reducibility and TT-lifting for computation types. In: TLCA, pp. 262\u2013277 (2005)","DOI":"10.1007\/11417170_20"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Mathematical Foundations of Programming Semantics","author":"Q. Ma","year":"1992","unstructured":"Ma, Q., Reynolds, J.: Types, abstractions, and parametric polymorphism, part 2. In: Schmidt, D., Main, M.G., Melton, A.C., Mislove, M.W., Brookes, S.D. (eds.) MFPS 1991. LNCS, vol.\u00a0598, pp. 1\u201340. Springer, Heidelberg (1992)"},{"key":"8_CR14","series-title":"Graduate Texts in Mathematics","volume-title":"Categories for theWorking Mathematician","author":"S. MacLane","year":"1998","unstructured":"MacLane, S.: Categories for theWorking Mathematician, 2nd edn. Graduate Texts in Mathematics, vol.\u00a05. Springer, Heidelberg (1998)","edition":"2"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Melli\u00e8s, P.-A., Vouillon, J.: Recursive polymorphic types and parametricity in an operational framework. In: Proc. LICS 2005 (2005) (to appear)","DOI":"10.1109\/LICS.2005.42"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Mitchell, J.: Representation independence and data abstraction. In: Proc. POPL, pp. 263\u2013276 (1986)","DOI":"10.1145\/512644.512669"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"1","key":"8_CR18","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-40018-9_24","volume-title":"Programming Languages and Systems","author":"S. Nishimura","year":"2003","unstructured":"Nishimura, S.: Correctness of a higher-order removal transformation through a relational reasoning. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol.\u00a02895, pp. 358\u2013375. Springer, Heidelberg (2003)"},{"issue":"4","key":"8_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":"8_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":"8_CR22","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"A. Pitts","year":"1998","unstructured":"Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 227\u2013273. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR23","first-page":"367","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G. Plotkin","year":"1980","unstructured":"Plotkin, G.: Lambda-definability in the full type hierarchy. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 367\u2013373. Academic Press, San Diego (1980)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Tait, W.: Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic\u00a032 (1967)","DOI":"10.2307\/2271658"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:13:42Z","timestamp":1605644022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11538363_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}