{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T21:11:28Z","timestamp":1768684288091,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We give a translation suitable for compilation of modern module calculi supporting sealing, generativity, translucent signatures, applicative functors, higher-order functors and\/or first-class modules. Ours is the first module-compilation translation with a dynamic correctness theorem. The theorem states that the translation produces target terms that are contextually equivalent to the source, in an appropriate sense. A corollary of the theorem is that the translation is fully abstract. Consequently, the translation preserves all abstraction present in the source. In passing, we also show that modules are a definitional extension of the underlying core language. All of our proofs are formalized in Coq.<\/jats:p>","DOI":"10.1145\/3290323","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Fully abstract module compilation"],"prefix":"10.1145","volume":"3","author":[{"given":"Karl","family":"Crary","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009892"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301641"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001134"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317800"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317800"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169696"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_2_2_14_1","volume-title":"Pierce","author":"Harper Robert","year":"2005","unstructured":"Robert Harper and Benjamin C . Pierce . 2005 . Design Considerations for ML-Style Module Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press . Robert Harper and Benjamin C. Pierce. 2005. Design Considerations for ML-Style Module Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press."},{"key":"e_1_2_2_15_1","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"Harper Robert","unstructured":"Robert Harper and Chris Stone . 2000. A Type-Theoretic Interpretation of Standard ML . In Proof, Language and Interaction: Essays in Honour of Robin Milner . The MIT Press . Extended version published as CMU technical report CMU-CS-97-147. Robert Harper and Chris Stone. 2000. A Type-Theoretic Interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner. The MIT Press. Extended version published as CMU technical report CMU-CS-97-147."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199476"},{"key":"e_1_2_2_19_1","unstructured":"Xavier Leroy. 2003. A proposal for recursive modules in Objective Caml. (2003). Available at http:\/\/caml.inria.fr\/pub\/papers\/ xleroy- recursive_modules- 03.pdf .  Xavier Leroy. 2003. A proposal for recursive modules in Objective Caml. (2003). Available at http:\/\/caml.inria.fr\/pub\/papers\/ xleroy- recursive_modules- 03.pdf ."},{"key":"e_1_2_2_20_1","volume-title":"The OCaml system, release 4.03, Documentation and user\u2019s manual","author":"Leroy Xavier","unstructured":"Xavier Leroy , Damien Doligez , Jacques Garrigue , Didier R\u00e9my , and J\u00e9r\u00f4me Vouillon . 2016. The OCaml system, release 4.03, Documentation and user\u2019s manual . Institut National de Recherche en Informatique et Automatique (INRIA) . Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier R\u00e9my, and J\u00e9r\u00f4me Vouillon. 2016. The OCaml system, release 4.03, Documentation and user\u2019s manual. Institut National de Recherche en Informatique et Automatique (INRIA)."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_2_22_1","volume-title":"Fifth European Symposium on Programming (Lecture Notes in Computer Science)","volume":"788","author":"David","unstructured":"David B. MacQueen and Mads Tofte. 1994. A Semantics for Higher-order Functors . In Fifth European Symposium on Programming (Lecture Notes in Computer Science) , Vol. 788 . Springer, 409\u2013423. David B. MacQueen and Mads Tofte. 1994. A Semantics for Higher-order Functors. In Fifth European Symposium on Programming (Lecture Notes in Computer Science), Vol. 788. Springer, 409\u2013423."},{"key":"e_1_2_2_23_1","volume-title":"The Definition of Standard ML","author":"Milner Robin","unstructured":"Robin Milner , Mads Tofte , and Robert Harper . 1990. The Definition of Standard ML . The MIT Press , Cambridge, Massachusetts . Robin Milner, Mads Tofte, and Robert Harper. 1990. The Definition of Standard ML. The MIT Press, Cambridge, Massachusetts."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_2_25_1","volume-title":"Formal Approaches to Secure Compilation. Comput. Surveys","author":"Patrignani Marco","year":"2019","unstructured":"Marco Patrignani , Amal Ahmed , and Dave Clarke . 2019. Formal Approaches to Secure Compilation. Comput. Surveys ( 2019 ). To appear. Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal Approaches to Secure Compilation. Comput. Surveys (2019). To appear."},{"key":"e_1_2_2_26_1","volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Pitts Andrew","unstructured":"Andrew Pitts . 2005. Typed Operational Reasoning . In Advanced Topics in Types and Programming Languages, Benjamin C . Pierce (Ed.). The MIT Press , Chapter 7, 245\u2013289. Andrew Pitts. 2005. Typed Operational Reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, Chapter 7, 245\u2013289."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_2_29_1","article-title":"First-Class Structures for Standard ML","volume":"7","author":"Russo Claudio V.","year":"2000","unstructured":"Claudio V. Russo . 2000 . First-Class Structures for Standard ML . Nordic Journal of Computing 7 , 4 (2000). Claudio V. Russo. 2000. First-Class Structures for Standard ML. Nordic Journal of Computing 7, 4 (2000).","journal-title":"Nordic Journal of Computing"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507644"},{"key":"e_1_2_2_31_1","volume-title":"Higher-order modules in System F \u03c9 and Haskell. (May","year":"2006","unstructured":"Chung-chieh Shan. 2006. Higher-order modules in System F \u03c9 and Haskell. (May 2006 ). Available at homes.soic.indiana. edu\/ccshan\/xlate\/xlate.pdf . Chung-chieh Shan. 2006. Higher-order modules in System F \u03c9 and Haskell. (May 2006). Available at homes.soic.indiana. edu\/ccshan\/xlate\/xlate.pdf ."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289436"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317801"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325724"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290323","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290323","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290323"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290323"],"URL":"https:\/\/doi.org\/10.1145\/3290323","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}