{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:28:13Z","timestamp":1725550093551},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119989"},{"type":"electronic","value":"9783642119996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11999-6_7","type":"book-chapter","created":{"date-parts":[[2010,3,16]],"date-time":"2010-03-16T04:52:29Z","timestamp":1268715149000},"page":"96-110","source":"Crossref","is-referenced-by-count":0,"title":["Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types"],"prefix":"10.1007","author":[{"given":"Yuki","family":"Kato","sequence":"first","affiliation":[]},{"given":"Koji","family":"Nakazawa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","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. Journal of Functional Programming\u00a010, 412\u2013452 (2000)","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"7_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":"7_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":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-44929-9_35","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"K. Fujita","year":"2000","unstructured":"Fujita, K., Schubert, A.: Partially Typed Terms between Church-Style and Curry-Style. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 505\u2013520. Springer, Heidelberg (2000)"},{"key":"7_CR5","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)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-02273-9_10","volume-title":"Typed Lambda Calculi and Applications","author":"K. Fujita","year":"2009","unstructured":"Fujita, K., Schubert, A.: Existential Type Systems with No Types in Terms. In: Curien, P.-L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol.\u00a05608, pp. 112\u2013126. Springer, Heidelberg (2009)"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BF01019463","volume":"6","author":"R. Harper","year":"1993","unstructured":"Harper, R., Lillibridge, M.: Polymorphic Type Assignment and CPS Conversion. Lisp and Symbolic Computation\u00a06, 361\u2013380 (1993)","journal-title":"Lisp and Symbolic Computation"},{"issue":"3:3","key":"7_CR8","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":"7_CR9","unstructured":"Hasegawa, M.: (2007) (unpublished manuscript)"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1006\/inco.1993.1003","volume":"102","author":"A.J. Kfoury","year":"1993","unstructured":"Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: The Undecidability of the Semi-unification Problem. Information and Computation\u00a0102, 83\u2013101 (1993)","journal-title":"Information and Computation"},{"issue":"3","key":"7_CR11","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":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-540-87531-4_34","volume-title":"Computer Science Logic","author":"K. Nakazawa","year":"2008","unstructured":"Nakazawa, K., Tatsuta, M., Kameyama, Y., Nakano, H.: Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 478\u2013492. Springer, Heidelberg (2008)"},{"key":"7_CR13","unstructured":"Nakazawa, K., Tatsuta, M.: Type Checking and Inference for Polymorphic and Existential Types. In: 15th Computing: the Australasian Theory Symposium (CATS 2009), Conferences in Research and Practice in Information Technology (CRPIT), vol. 94 (2009)"},{"key":"7_CR14","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":"7_CR15","doi-asserted-by":"crossref","unstructured":"Schubert, A.: Second-order unification and type inference for Church-style polymorphism. In: 25th Annual ACM Symposium on Principles of Programming Languages (POPL 1998), pp. 279\u2013288 (1998)","DOI":"10.1145\/268946.268969"},{"key":"7_CR16","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":"7_CR17","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":"7_CR18","unstructured":"Thielecke, H.: Categorical Structure of Continuation Passing Style. Ph.D. Thesis, University of Edinburgh (1997)"},{"key":"7_CR19","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","Functional and Constraint Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11999-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:16Z","timestamp":1606185976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11999-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119989","9783642119996"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11999-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}