一句话：提出首个具有动态正确性定理的模块编译翻译，证明其完全抽象并保持源语言抽象性。
现代模块演算通常支持密封、生成性、透明签名、应用式函子、高阶函子和/或一等模块，但为其设计具有动态正确性的编译翻译一直困难。本文给出一种适用于此类模块演算编译的翻译，并证明该翻译产生的目标项在适当意义下与源项上下文等价，因而具有完全抽象性；推论是翻译保持源语言中所有抽象。论文还表明模块可视为底层核心语言的定义式扩展。所有证明均在 Coq 中形式化。
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.