{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:15:44Z","timestamp":1725459344084},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037122","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"418-432","source":"Crossref","is-referenced-by-count":4,"title":["Type reconstruction in F\u03c9 is undecidable"],"prefix":"10.1007","author":[{"given":"Pawe\u0142","family":"Urzyczyn","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., Hemerik, K., Types in lambda calculi and programming languages, Proc. ESOP'90, pp. 1\u201335.","DOI":"10.1007\/3-540-52592-0_53"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Partial polymorphic type inference is undecidable, Proc. 26th FOCS, 1985, pp. 339\u2013345.","DOI":"10.1109\/SFCS.1985.44"},{"key":"29_CR3","unstructured":"Coquand, T., Metamathematical investigations of a calculus of constructions, in: Logic in Computer Science (Odifreddi, ed.), Acad. Press, 1990, pp. 91\u2013122."},{"key":"29_CR4","unstructured":"Gallier, J. H., On Girard's \u201cCandidats de Reductibilit\u00e9\u201d, in: Logic in Computer Science, (Odifreddi, ed.), Acad. Press, 1990, pp. 123\u2013203."},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Giannini, P., Ronchi Della Rocca, S., Characterization of typings in polymorphic type discipline, Proc. 3rd LICS, 1988, pp. 61\u201370.","DOI":"10.1109\/LICS.1988.5101"},{"key":"29_CR6","series-title":"LNCS 526","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-54415-1_39","volume-title":"Proc. Theoretical Aspects of Computer Software","author":"P. Giannini","year":"1991","unstructured":"Giannini, P., Ronchi Della Rocca, S., Type inference in polymorphic type discipline, Proc. Theoretical Aspects of Computer Software (Ito, Meyer, eds.), LNCS 526, Springer, Berlin, 1991, pp. 18\u201337."},{"key":"29_CR7","unstructured":"Giannini, P., Ronchi Della Rocca, S., Honsell, F., Type inference: some results, some problems, manuscript, 1992, to appear in Fundamenta Informaticae."},{"key":"29_CR8","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"Girard, J.-Y., The system F of variable types fifteen years later Theoret. Comput. Sci., 45 (1986), 159\u2013192.","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR9","unstructured":"Henglein, F., A lower bound for full polymorphic type inference: Girard\/Reynolds typability is DEXPTIME-hard, Technical Report RUU-CS-90-14, University of Utrecht, April 1990."},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Henglein, F., Mairson, H.G., The complexity of type inference for higher-order typed lambda calculi, Proc. 18th POPL, 1991, pp. 119\u2013130.","DOI":"10.1145\/99583.99602"},{"issue":"No.2","key":"29_CR11","doi-asserted-by":"crossref","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, vol. 98, No. 2, 1992, 228\u2013257.","journal-title":"Information and Computation"},{"key":"29_CR12","unstructured":"Kfoury, A.J., Tiuryn, J. and Urzyczyn, P., An analysis of ML typability, to appear in Journal of the ACM (preliminary version in Proc. CAAP\/ESOP'90)."},{"key":"29_CR13","unstructured":"Kfoury, A.J., Tiuryn, J. and Urzyczyn, P., The undecidability of the semiunification problem, to appear in Information and Computation (preliminary version in Proc. STOC'90)."},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Kanellakis, P.C., Mitchell, J.C., Polymorphic unification and ML typing, Proc. 16th POPL, 1989, pp. 105\u2013115.","DOI":"10.1145\/75277.75286"},{"key":"29_CR15","unstructured":"Kanellakis, P.C., Mairson H.G.; Mitchell J.C., Unification and ML type reconstruction, Chapter 13 in Computational Logic, Essays in Honor of Alan J. Robinson, (J-L. Lassez and G. Plotkin eds), MIT Press, 1991."},{"key":"29_CR16","first-page":"123","volume":"304","author":"J.L. Krivine","year":"1987","unstructured":"Krivine, J.L., Un algorithme non typable dans le syst\u00e8me F, F.C.R. Acad. Sci. Paris, S\u00e9rie I, 304 (1987), 123\u2013126.","journal-title":"F.C.R. Acad. Sci. Paris, S\u00e9rie I"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Leivant, D., Polymorphic type inference, Proc. 10th POPL, 1983, pp. 88\u201398.","DOI":"10.1145\/567067.567077"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Mairson, H.G., Deciding ML typability is complete for deterministic exponential time, Proc. 17th POPL, 1990, pp. 382\u2013401.","DOI":"10.1145\/96709.96748"},{"key":"29_CR19","series-title":"LNCS 443","first-page":"46","volume-title":"Proc. 17th ICALP","author":"S. Malecki","year":"1990","unstructured":"Malecki, S., Generic terms having no polymorphic types, Proc. 17th ICALP, LNCS 443, Springer, Berlin, 1990, pp. 46\u201359."},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Partial polymorphic type inference and higher-order unification, Proc. Lisp and Functional Programming, 1988, pp. 153\u2013163.","DOI":"10.1145\/62678.62697"},{"key":"29_CR21","unstructured":"Pierce, B., Dietzen, S., Michaylov, S., Programming in higher-order typed lambda calculi, Research Report CMU-CS-89-111, Carnegie-Mellon University, 1989."},{"key":"29_CR22","unstructured":"Urzyczyn, P., Type reconstruction in F \u03c9, Research Report BU-CS-92-014, Boston University, 1992."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037122.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:11Z","timestamp":1607552531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0037122","relation":{},"subject":[]}}