{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:40:52Z","timestamp":1737006052385,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678236"},{"type":"electronic","value":"9783540449294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44929-9_35","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T13:20:53Z","timestamp":1178371253000},"page":"505-520","source":"Crossref","is-referenced-by-count":3,"title":["Partially Typed Terms between Church-Style and Curry-Style"],"prefix":"10.1007","author":[{"given":"Ken-Etsu","family":"Fujita","sequence":"first","affiliation":[]},{"given":"Aleksy","family":"Schubert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"35_CR1","first-page":"1","volume":"II","author":"H. P. Barendregt","year":"1992","unstructured":"Barendregt, H. P.: Lambda Calculi with Types, Handbook of Logic in Computer Science Vol. II, Oxford University Press, pp. 1\u2013189, 1992.","journal-title":"Handbook of Logic in Computer Science"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Boehm, Hans-J.: Partial Polymorphic Type Inference is Undecidable, Proc. 26th Annual Symposium of Fundations of Computer Science, pp. 339\u2013345, 1985.","DOI":"10.1109\/SFCS.1985.44"},{"key":"35_CR3","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M. H.: CSP Translations and Applications: The Cube and Beyond, Proc. ACM SIGPLAN on Continuations, pp. 1\u201331, 1996."},{"key":"35_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/3-540-63045-7_2","volume-title":"Logical Foundations of Computer Science","author":"G. Barthe","year":"1997","unstructured":"Barthe, G. and S\u00f8rensen, M. H.: Domain-Free Pure Type Systems, Lecture Notes in Computer Science 1234, pp. 9\u201320, 1997."},{"key":"35_CR5","unstructured":"Barthe, G. and S\u00f8rensen, M. H.: Domain-Free Pure Type Systems."},{"key":"35_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic, Vol. 5, pp. 56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"35_CR7","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"H. B. Curry","year":"1934","unstructured":"Curry, H. B.: Functionality in combinatory logic, Proc. National Academy of Sciences of the USA 20, pp. 584\u2013590, 1934.","journal-title":"Proc. National Academy of Sciences of the USA"},{"key":"35_CR8","unstructured":"Curry, H. B., Feys, R. and Craig, W.: Combinatory Logic, Volume 1 (Third printing), North-Holland, 1974."},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Damas, L. and Milner, R.: Principal type-schemes for functional programs, Proc. ACM Symposium on Principles of Programming Languages, pp. 207\u2013212, 1982.","DOI":"10.1145\/582153.582176"},{"key":"35_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-48959-2_13","volume-title":"Typed Lambda Calculi and Applications: 4th International Conference, TLCA\u201999, L\u2019Aquilla, Italy, April 1999.","author":"K. Fujita","year":"1999","unstructured":"Fujita, K.: Explicitly Typed \u03bb\u03bc-Calculus for Polymorphism and Call-by-Value, Lecture Notes in Computer Science 1581, pp. 162\u2013176, 1999."},{"key":"35_CR11","unstructured":"Fujita, K.: Type Inference for Domain-Free \u03bb2, Technical Report in Computer Science and Systems Engineering CSSE-5, Kyushu Institute of Technology, 1999."},{"key":"35_CR12","first-page":"40","volume":"17","author":"K. Fujita","year":"2000","unstructured":"Fujita, K: Undecidability of Partial Type Reconstruction, Computer Software, Vol. 17, No. 2, pp. 40\u201344, 2000 (in Japanese).","journal-title":"Computer Software"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Garrigue, J. and R\u00e9my, D.: Semi-Explicit First-Class Polymorphism for ML, Information and Computation, 1999.","DOI":"10.1006\/inco.1999.2830"},{"key":"35_CR14","unstructured":"Harper, R. and Lillibridge, M.: ML with callcc is unsound, The Types Form, 8 July 1991."},{"key":"35_CR15","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/169701.169696","volume":"15","author":"R. Harper","year":"1993","unstructured":"Harper, R. and Mitchell, J. C.: On The Type Structure of Standard ML, ACM Trans. on Programming Languages and Systems, Vol. 15, No. 2, pp. 210\u2013252, 1993.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"35_CR16","doi-asserted-by":"crossref","unstructured":"Hindley, J. R.: Basic Simple Type Theory, Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511608865"},{"key":"35_CR17","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/0890-5401(92)90020-G","volume":"98","author":"A. J. Kfoury","year":"1992","unstructured":"Kfoury, A. J. and Tiuryn, J.: Type Reconstruction in Finite Rank Fragments of the Second-Order \u03bb-Calculus, Information and Computation 98, pp. 228\u2013257, 1992.","journal-title":"Information and Computation"},{"key":"35_CR18","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1145\/174652.174659","volume":"41","author":"A. J. Kfoury","year":"1994","unstructured":"Kfoury, A. J., Tiuryn, J. and Urzyczyn, P.: An Analysis of ML Typability, Journal of the Association for Computing Machinery, Vol. 41, No. 2, pp. 368\u2013398, 1994.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"Kfoury, A. J. and Wells, J. B.: A direct algorithm for type inference in the rank-2 fragment of the second-order \u03bb-calculus, Proc. ACM LISP and Functional Programming, pp. 196\u2013207, 1994.","DOI":"10.1145\/182409.182456"},{"key":"35_CR20","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0890-5401(91)90053-5","volume":"93","author":"D. Leivant","year":"1991","unstructured":"Leivant, D.: Finitely Stratified Polymorphism, Information and Computation 93, pp. 93\u2013113, 1991.","journal-title":"Information and Computation"},{"key":"35_CR21","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A Theory of Type Polymorphism in Programming, Journal of Computer and System Sciences 17, pp. 348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"Odersky, M. and L\u00e4ufer, K.: Putting Type Annotations to Work, Proc. ACM Symposium on Principles of Programming Languages, pp. 54\u201376, 1996.","DOI":"10.1145\/237721.237729"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"Ohori, A. and Yoshida, N.: Type Inference with Rank 1 Polymorphism for Type-Directed Compilation for ML, Proc. ACM Conference on Functional Programming, pp. 160\u2013171, 1999.","DOI":"10.1145\/317636.317796"},{"key":"35_CR24","series-title":"Lect Notes Comput Sci","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, Lecture Notes in Computer Science 624, pp. 190\u2013201, 1992."},{"key":"35_CR25","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Partial polymorphic type inference and higher-order unification, Proc. ACM Conference on Lisp and Functional Programming, pp. 153\u2013163, 1998.","DOI":"10.1145\/62678.62697"},{"key":"35_CR26","doi-asserted-by":"crossref","first-page":"185","DOI":"10.3233\/FI-1993-191-208","volume":"19","author":"F. Pfenning","year":"1993","unstructured":"Pfenning, F.: On the undecidability of partial polymorphic type reconstruction, Fundamenta Informaticae 19, pp. 185\u2013199, 1993.","journal-title":"Fundamenta Informaticae"},{"key":"35_CR27","unstructured":"Pfenning, F.: private communication, 9 June 1999."},{"key":"35_CR28","unstructured":"Schubert, A.: Second-order unification and type inference for Church-style, Tech. Report TR 97-02 (239), Institute of Informatics, Warsaw University, January 1997."},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Schubert, A.: Second-order unification and type inference for Church-style, Proc. ACM Symposium on Principles of Programming Languages, pp. 279\u2013288, 1998.","DOI":"10.1145\/268946.268969"},{"key":"35_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BFb0029599","volume-title":"Type Inference Problems: A Survey","author":"J. Tiuryn","year":"1990","unstructured":"Tiuryn, J.: Type Inference Problems: A Survey, Lecture Notes in Computer Science 452, pp. 105\u2013120, 1990."},{"key":"35_CR31","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L. S. Benthem Jutting Van","year":"1993","unstructured":"Van Benthem Jutting, L. S.: Typing in Pure Type Systems, Information and Computation 105, pp. 30\u201341, 1993.","journal-title":"Information and Computation"},{"key":"35_CR32","doi-asserted-by":"crossref","unstructured":"Wells, J. B.: Typability and Type Checking in the Second-Order \u03bb-Calculus Are Equivalent and Undecidable, Proc. IEEE Symposium on Logic in Computer Science, pp. 176\u2013185, 1994.","DOI":"10.1109\/LICS.1994.316068"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44929-9_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T02:15:33Z","timestamp":1736993733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44929-9_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678236","9783540449294"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-44929-9_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}