{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:15Z","timestamp":1776891435737,"version":"3.51.2"},"reference-count":28,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T00:00:00Z","timestamp":1481500800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The connection between polymorphic and dynamic typing was originally considered\n                    by Curry\n                    <jats:italic>et al.<\/jats:italic>\n                    (1972,\n                    <jats:italic>Combinatory Logic<\/jats:italic>\n                    , vol.\n                    ii) in the form of \u201cpolymorphic type assignment\u201d for untyped\n                    \u03bb-terms. Types are assigned after the fact to what is, in modern\n                    terminology, a dynamic language. Interest in type assignment was revitalized by\n                    the proposals of Bracha\n                    <jats:italic>et al.<\/jats:italic>\n                    (1998, OOPSLA) and Bank\n                    <jats:italic>et al.<\/jats:italic>\n                    (1997, POPL) to enrich Java with polymorphism\n                    (generics), which in turn sparked the development of other languages, such as\n                    Scala, with similar combinations of features. In such a setting, where the\n                    target language already has a monomorphic type system, it is desirable to\n                    compile polymorphism to dynamic typing in such a way that as much static typing\n                    as possible is preserved, relying on dynamics only insofar as genericity is\n                    actually required. The basic approach is to compile polymorphism using\n                    embeddings from each type into a universal \u201ctop\u201d type,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0956796816000265_inline1\"\/>\n                        <jats:tex-math>${\\mathbb{D}}$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , and partial projections that go in the\n                    other direction. This scheme is intuitively reasonable, and, indeed, has been\n                    used in practice many times. Proving its correctness, however, is non-trivial.\n                    This paper studies the compilation of System\n                    <jats:monospace>F<\/jats:monospace>\n                    to an\n                    extension of Moggi's computational meta-language with a dynamic type and shows\n                    how the compilation may be proved correct using a logical relation.\n                  <\/jats:p>","DOI":"10.1017\/s0956796816000265","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T06:13:58Z","timestamp":1481523238000},"source":"Crossref","is-referenced-by-count":1,"title":["Correctness of compiling polymorphism to dynamic typing"],"prefix":"10.46298","volume":"27","author":[{"given":"KUEN-BANG","family":"HOU (Favonia)","sequence":"first","affiliation":[]},{"given":"NICK","family":"BENTON","sequence":"additional","affiliation":[]},{"given":"ROBERT","family":"HARPER","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,12,12]]},"reference":[{"key":"S0956796816000265_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"S0956796816000265_ref16","unstructured":"McCracken N. 1979 (June) An Investigation of a Programming Language with a Polymorphic Type Structure. Ph.D. thesis, Syracuse University."},{"key":"S0956796816000265_ref26","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (1974) Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation. Berlin, Heidelberg: Springer-Verlag, pp. 408\u2013423.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0956796816000265_ref24","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1017\/S0956796811000219","article-title":"Embedding an interpreted language\n                        using higher-order functions and types","volume":"21","author":"Ramsey","year":"2011","journal-title":"J. Funct.\n                        Program."},{"key":"S0956796816000265_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_17"},{"key":"S0956796816000265_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"S0956796816000265_ref14","unstructured":"Hur C.-K. , & Dreyer D. (2011) A Kripke logical relation between ML and assembly. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). New York, NY, USA: ACM, pp. 133\u2013146."},{"key":"S0956796816000265_ref22","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"S0956796816000265_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449798"},{"key":"S0956796816000265_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005398"},{"key":"S0956796816000265_ref10","volume-title":"Combinatory Logic, Volume ii","author":"Curry","year":"1972"},{"key":"S0956796816000265_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"S0956796816000265_ref8","doi-asserted-by":"crossref","unstructured":"Bracha G. , Odersky M. , Stoutamire D. & Wadler P. (1998) Making the future safe for the past: adding genericity to the Java programming language. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA '98), vol. 33. New York, NY, USA: ACM, pp. 183\u2013200.","DOI":"10.1145\/286936.286957"},{"key":"S0956796816000265_ref25","first-page":"513","volume-title":"Information Processing 83","author":"Reynolds","year":"1983"},{"key":"S0956796816000265_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263714"},{"key":"S0956796816000265_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0956796816000265_ref12","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris 7."},{"key":"S0956796816000265_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139342131"},{"key":"S0956796816000265_ref11","unstructured":"Findler R. B. & Felleisen M. (2002) Contracts for higher-order functions. In Proceedings of the International Conference on Functional Programming (ICFP). New York, NY, USA: ACM, pp. 48\u201359. doi = 10.1145\/581478.581484."},{"key":"S0956796816000265_ref3","doi-asserted-by":"crossref","unstructured":"Amadio R. (1993) On the adequacy of PER models. In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 711. Berlin, Heidelberg: Springer, pp. 222\u2013231.","DOI":"10.1007\/3-540-57182-5_14"},{"key":"S0956796816000265_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796816000265_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796816000265_ref7","unstructured":"Benton N. & Hur C.-K. (2010) Realizability and Compositional Compiler Correctness for a Polymorphic Language. Technical Report, MSR-TR-2010-62. Microsoft Research."},{"key":"S0956796816000265_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"S0956796816000265_ref28","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0956796816000265_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"S0956796816000265_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708028"},{"key":"S0956796816000265_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:50Z","timestamp":1776889190000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000265\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,12]]},"references-count":28,"alternative-id":["S0956796816000265"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000265","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,12]]},"article-number":"e1"}}