{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:59:50Z","timestamp":1742950790216,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"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_34","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"478-492","source":"Crossref","is-referenced-by-count":3,"title":["Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence"],"prefix":"10.1007","author":[{"given":"Koji","family":"Nakazawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Makoto","family":"Tatsuta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yukiyoshi","family":"Kameyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Nakano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1017\/S0956796800003750","volume":"10","author":"G. Barthe","year":"2000","unstructured":"Barthe, G., S\u00f8rensen, M.H.: Domain-free pure type systems. J. Functional Programming\u00a010, 412\u2013452 (2000)","journal-title":"J. Functional Programming"},{"issue":"4","key":"34_CR2","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Danvy, O., Fillinski, A.: Representing Control: a Study of the CPS Translation. Mathematical Structures in Computer Science\u00a02(4), 361\u2013391 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-48959-2_13","volume-title":"Typed Lambda Calculi and Applications","author":"K. Fujita","year":"1999","unstructured":"Fujita, K.: Explicitly typed \u03bb\u03bc-calculus for polymorphism and call-by-value. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 162\u2013177. Springer, Heidelberg (1999)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/11417170_15","volume-title":"Typed Lambda Calculi and Applications","author":"K. Fujita","year":"2005","unstructured":"Fujita, K.: Galois embedding from polymorphic types in to existential types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 194\u2013208. Springer, Heidelberg (2005)"},{"issue":"3:3","key":"34_CR5","first-page":"1","volume":"2","author":"M. Hasegawa","year":"2006","unstructured":"Hasegawa, M.: Relational parametricity and control. Logical Methods in Computer Science\u00a02(3:3), 1\u201322 (2006)","journal-title":"Logical Methods in Computer Science"},{"key":"34_CR6","unstructured":"Hasegawa, M.: (unpublished manuscript, 2007)"},{"issue":"3","key":"34_CR7","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J.C. Mitchell","year":"1988","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems\u00a010(3), 470\u2013502 (1988)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of 4th Annual Symposium on Logic in Computer Science (LICS 1989), pp. 14\u201323 (1989)","DOI":"10.1109\/LICS.1989.39155"},{"key":"34_CR9","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":"34_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G.: Call-by-name, call-by-value, and the \u03bb-calculus. Theoretical Computer Science\u00a01, 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"34_CR11","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A. Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems\u00a019(6), 916\u2013941 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73228-0_26","volume-title":"Typed Lambda Calculi and Applications","author":"M. Tatsuta","year":"2007","unstructured":"Tatsuta, M.: Simple saturated sets for disjunction and second-order existential quantification. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 366\u2013380. Springer, Heidelberg (2007)"},{"key":"34_CR13","unstructured":"Tatsuta, M., Fujita, K., Hasegawa, R., Nakano, H.: Inhabitance of Existential Types is Decidable in Negation-Product Fragment. In: Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC 2008) (2008)"},{"key":"34_CR14","unstructured":"Thielecke, H.: Categorical Structure of Continuation Passing Style. Ph.D. Thesis, University of Edinburgh (1997)"},{"key":"34_CR15","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L.S. van Benthem Jutting","year":"1993","unstructured":"van Benthem Jutting, L.S.: Typing in pure type systems. Information and Computation\u00a0105, 30\u201341 (1993)","journal-title":"Information and Computation"},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"Wells, J.B.: Typability and type checking in the second-order \u03bb-calculus are equivalent and undecidable. In: Proceedings of 9th Symposium on Logic in Computer Science (LICS 1994), pp. 176\u2013185 (1994)","DOI":"10.1109\/LICS.1994.316068"}],"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_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T19:04:42Z","timestamp":1738350282000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}