{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:22Z","timestamp":1725665002852},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631729"},{"type":"electronic","value":"9783540692010"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63172-0_46","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:16:11Z","timestamp":1330280171000},"page":"297-315","source":"Crossref","is-referenced-by-count":0,"title":["Proofs in system F \u03c9 can be done in system F \u03c91"],"prefix":"10.1007","author":[{"given":"Sophie","family":"Malecki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Boehm, H. J.: Partial polymorphic type inference is undecidable. 26th Annual Symposium on Foundations of Computer Science IEEE Press (1985) 339\u2013345","DOI":"10.1109\/SFCS.1985.44"},{"key":"18_CR2","unstructured":"Gallier, J. H.: On Girard's Candidats de Reductibilite. Logic and Computer Science Academic Press P. Odifreddi (1990) 123\u2013204"},{"key":"18_CR3","unstructured":"Giannini, P., Ronchi Della Rocca, S.: Characterization of typings in polymorphic type disscipline. Proc. 3rd Ann. Symp. Logic Comput. Sci. Edinburgh (1988) 61\u201370"},{"issue":"12","key":"18_CR4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/FI-1993-191-205","volume":"19","author":"P. Giannini","year":"1993","unstructured":"Giannini, P., Honsell, F., Ronchi Della Rocca, S.: Type Inference: Some results, Some problems. Fondamenta Informaticae 19(1,2) (1993) 87\u2013125","journal-title":"Some problems. Fondamenta Informaticae"},{"key":"18_CR5","unstructured":"Girard, J.Y.: Interpretation Fonctionnelle et Elimination des Coupures de l'Arithm\u00e9tique d'Ordre Sup\u00e9rieure. Th\u00e8se d'etat Universit\u00e9 Paris VII (1972)"},{"key":"18_CR6","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. Goldfarb","year":"1981","unstructured":"Goldfarb, W.: The Undecidability of the Second-Order Unification Problem. TCS 13 (1981) 225\u2013230","journal-title":"TCS"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Gould, W. E.: A Matching Procedure for Omega-Order Logic. Princeton University (1966)","DOI":"10.21236\/AD0646560"},{"key":"18_CR8","first-page":"29","volume":"146","author":"J. R. Hindley","year":"1969","unstructured":"Hindley, J. R.: The Principal Type Scheme of an Object in Combinatory Logic. Trans. Am. Math. Soc. 146 (1969) 29\u201360","journal-title":"Trans. Am. Math. Soc."},{"key":"18_CR9","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"Huet, G.: The Undecidability of Unification in Third-Order Logic. Information and Control (22) (1973) 257\u2013267","journal-title":"Information and Control"},{"key":"18_CR10","unstructured":"Malecki, S.: Quelques R\u00e9sultats sur la Typabilit\u00e9 dans le Syst\u00e8me F. Th\u00e8se de Doctorat Universit\u00e9 Paris VII (1992)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Partial polymorphic type inference and higher order unification. ACM LISP and Functional Programming Conference (1988) 153\u2013163","DOI":"10.1145\/62678.62697"},{"key":"18_CR12","unstructured":"Reynolds, J. C.: Towards a Theory of Type Structures. Paris Colloquium on Programming, Springer-Verlag, (1974) 408\u2013425"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Snyder, W.: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic (1991)","DOI":"10.1007\/978-1-4612-0435-0"},{"key":"18_CR14","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/BFb0037122","volume":"664","author":"P. Urzyczyn","year":"1993","unstructured":"Urzyczyn, P.: Type reconstruction in F \u03c9 is undecidable. Int'l Conf. Typed Lambda Calculi and Applications Springer-Verlag 664 (1993) 418\u2013432","journal-title":"Typed Lambda Calculi and Applications Springer-Verlag"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Wells, J.B.: Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable. Eight Annual IEEE Symposium on Logic in Computer Science IEEE Press (1994)","DOI":"10.1109\/LICS.1994.316068"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63172-0_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T06:39:15Z","timestamp":1640932755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63172-0_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631729","9783540692010"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-63172-0_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}