{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:17:39Z","timestamp":1750306659134,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"4S","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain secondorder type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred. All expressions of ML are welltyped without any annotations. All expressions of System F can be mechanically encoded into MLF by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into MLF types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.<\/jats:p>","DOI":"10.1145\/2641638.2641653","type":"journal-article","created":{"date-parts":[[2014,7,8]],"date-time":"2014-07-08T12:20:08Z","timestamp":1404822008000},"page":"52-63","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["MLF"],"prefix":"10.1145","volume":"49","author":[{"given":"Didier","family":"Le Botlan","sequence":"first","affiliation":[{"name":"INRIA-Rocquencourt, France"}]},{"given":"Didier","family":"R\u00e9my","sequence":"additional","affiliation":[{"name":"INRIA-Rocquencourt, France"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1109\/SFCS.1985.44"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.5555\/527211"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_5_1","first-page":"259","volume-title":"Joint international conference and symposium on logic programming","author":"Dowek G.","year":"1996"},{"unstructured":"J. Garrigue. Relaxing the value-restriction. Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS) 2002.  J. Garrigue. Relaxing the value-restriction. Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS) 2002.","key":"e_1_2_1_6_1"},{"issue":"1","key":"e_1_2_1_7_1","first-page":"134","article-title":"Extending ML with semi-explicit higher-order polymorphism","volume":"155","author":"Garrigue J.","year":"1999","journal-title":"Journal of Functional Programming"},{"unstructured":"The GHC Team. The Glasgow Haskell Compiler User's Guide Version 5.04 2002. Chapter Arbitrary-rank polymorphism.  The GHC Team. The Glasgow Haskell Compiler User's Guide Version 5.04 2002. Chapter Arbitrary-rank polymorphism.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","first-page":"61","volume-title":"Third annual Symposium on Logic in Computer Science","author":"Giannini P.","year":"1988"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/74818.74836"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/237721.237728"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/182409.182456"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1145\/292540.292556"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/186025.186031"},{"volume-title":"INRIA","year":"2002","author":"Leroy X.","key":"e_1_2_1_16_1"},{"unstructured":"Mark P Jones Alastair Reid the Yale Haskell Group and the OGI School of Science & Engineering at OHSU. An overview of hugs extensions. Available electronically 1994--2002.  Mark P Jones Alastair Reid the Yale Haskell Group and the OGI School of Science & Engineering at OHSU. An overview of hugs extensions. Available electronically 1994--2002.","key":"e_1_2_1_17_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1016\/0747-7171(92)90011-R"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1016\/0890-5401(88)90009-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/237721.237729"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/373243.360207"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/62678.62697"},{"doi-asserted-by":"crossref","unstructured":"F. Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae 19(1 2):185--199 1993. Preliminary version available as Technical Report CMU-CS-92-105 School of Computer Science Carnegie Mellon University January 1992.   F. Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae 19(1 2):185--199 1993. Preliminary version available as Technical Report CMU-CS-92-105 School of Computer Science Carnegie Mellon University January 1992.","key":"e_1_2_1_23_1","DOI":"10.3233\/FI-1993-191-208"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/345099.345100"},{"doi-asserted-by":"crossref","unstructured":"D.\n       \n      R\u00e9my\n    .\n      \n  \n   \n  Programming objects with ML-ART: An extension to ML with abstract and record types. In M. Hagiya and J. C. Mitchell editors Theoretical Aspects of Computer Software volume \n  789\n   of \n  Lecture Notes in Computer Science pages \n  321\n  --\n  346\n  . \n  Springer-Verlag April \n  1994\n  .   D. R\u00e9my. Programming objects with ML-ART: An extension to ML with abstract and record types. In M. Hagiya and J. C. Mitchell editors Theoretical Aspects of Computer Software volume 789 of Lecture Notes in Computer Science pages 321--346. Springer-Verlag April 1994.","key":"e_1_2_1_25_1","DOI":"10.1007\/3-540-57887-0_102"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1109\/LICS.1994.316068","volume-title":"Ninth annual IEEE Symposium on Logic in Computer Science","author":"Wells J. B.","year":"1994"},{"volume-title":"Boston University","year":"1996","author":"Wells J. B.","key":"e_1_2_1_27_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/BF01018828"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2641638.2641653","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2641638.2641653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:56:19Z","timestamp":1750229779000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2641638.2641653"}},"subtitle":["raising ML to the power of system F"],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":26,"journal-issue":{"issue":"4S","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2641638.2641653"],"URL":"https:\/\/doi.org\/10.1145\/2641638.2641653","relation":{},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}