{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:55:58Z","timestamp":1760079358648,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540875307"},{"type":"electronic","value":"9783540875314"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_21","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"278-292","source":"Crossref","is-referenced-by-count":2,"title":["A Characterisation of Lambda Definability with Sums Via \u22a4\u2009\u22a4-Closure Operators"],"prefix":"10.1007","author":[{"given":"Shin-ya","family":"Katsumata","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1&2","key":"21_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0304-3975(94)00283-O","volume":"146","author":"M. Alimohamed","year":"1995","unstructured":"Alimohamed, M.: A characterization of lambda definability in categorical models of implicit polymorphism. Theor. Comput. Sci.\u00a0146(1&2), 5\u201323 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS, pp. 303\u2013310 (2001)","DOI":"10.1109\/LICS.2001.932506"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/964001.964007","volume-title":"POPL","author":"V. Balat","year":"2004","unstructured":"Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: Jones, N., Leroy, X. (eds.) POPL, pp. 64\u201376. ACM, New York (2004)"},{"key":"21_CR4","volume-title":"Toposes, Triples and Theories","author":"M. Barr","year":"1998","unstructured":"Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (1998)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11575467_24","volume-title":"Programming Languages and Systems","author":"N. Benton","year":"2005","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"21_CR6","series-title":"Encyclopedia of Mathematics and Its Applications","volume-title":"Handbook of Categorical Algebra 1","author":"F. Borceux","year":"1994","unstructured":"Borceux, F.: Handbook of Categorical Algebra 1. Encyclopedia of Mathematics and Its Applications, vol.\u00a050. Cambridge University Press, Cambridge (1994)"},{"issue":"3","key":"21_CR7","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1017\/S0960129500000232","volume":"3","author":"J. Cockett","year":"1993","unstructured":"Cockett, J.: Introduction to distributive categories. Mathematical Structures in Computer Science\u00a03(3), 277\u2013307 (1993)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"21_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-4049(72)90021-7","volume":"2","author":"B. Day","year":"1972","unstructured":"Day, B.: A reflection theorem for closed categories. Journal of pure and applied algebra\u00a02(1), 1\u201311 (1972)","journal-title":"Journal of pure and applied algebra"},{"key":"21_CR9","first-page":"282","volume-title":"LICS","author":"D. Dougherty","year":"1995","unstructured":"Dougherty, D., Subrahmanyam, R.: Equality between functionals in the presence of coproducts. In: LICS, pp. 282\u2013291. IEEE Computer Society, Los Alamitos (1995)"},{"key":"21_CR10","first-page":"147","volume-title":"LICS","author":"M. Fiore","year":"2002","unstructured":"Fiore, M., Di Cosmo, R., Balat, V.: Remarks on isomorphisms in typed lambda calculi with empty and sum types. In: LICS, pp. 147\u2013157. IEEE Computer Society, Los Alamitos (2002)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-48959-2_12","volume-title":"Typed Lambda Calculi and Applications","author":"M. Fiore","year":"1999","unstructured":"Fiore, M., Simpson, A.: Lambda definability with sums via grothendieck logical relations. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 147\u2013161. Springer, Heidelberg (1999)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BFb0014052","volume-title":"Typed Lambda Calculi and Applications","author":"N. Ghani","year":"1995","unstructured":"Ghani, N.: \u03b2\u03b7-equality for coproducts. In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 171\u2013185. Springer, Heidelberg (1995)"},{"key":"21_CR13","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":"21_CR14","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"21_CR15","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":"21_CR16","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":"21_CR17","unstructured":"Lafont, Y.: Logiques, Categ\u00f3ries et Machines. PhD thesis, Universit\u2018\u2019e Paris VII (1988)"},{"key":"21_CR18","unstructured":"Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. In: Cambridge studies in advanced mathematics. CUP (1986)"},{"key":"21_CR19","unstructured":"Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2004)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"21_CR21","first-page":"82","volume-title":"Proc. LICS 2005","author":"P.-A. Melli\u00e8s","year":"2005","unstructured":"Melli\u00e8s, P.-A., Vouillon, J.: Recursive polymorphic types and parametricity in an operational framework. In: Proc. LICS 2005, pp. 82\u201391. IEEE Computer Society, Los Alamitos (2005)"},{"key":"21_CR22","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"},{"issue":"4","key":"21_CR23","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":"21_CR24","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":"21_CR25","series-title":"Publications of the Newton Institute","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":"21_CR26","series-title":"Cambridge Computer Science Texts","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511608872","volume-title":"Categories and Computer Science","author":"R.F.C. Walters","year":"1992","unstructured":"Walters, R.F.C.: Categories and Computer Science. Cambridge Computer Science Texts. Cambridge University Press, Cambridge (1992)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T19:04:37Z","timestamp":1738350277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}