一句话：用聚焦逻辑为 ML 模块类型论中的 avoidance 问题建立存在签名元理论，并在 Coq 中形式化。
在 ML 风格模块类型论中，sealing 会使类型变量离开作用域，因此需要避免这些变量的签名；但一般不存在最佳此类签名，导致模块不总有主签名，即 avoidance 问题。已有工作通过移动变量使其保持作用域的机制来规避该问题，但缺少逻辑基础，且未在同一语法上同时给出静态与动态语义，限制了应用。本文按定义加入存在签名，使其成为其实例的最小上界，从而构造最佳 super-signature，并借助聚焦逻辑的思想解决元理论难题。新理论得到的类型规则与既有机制高度相似，还为 ML 模块静态语义早期的生成戳提供类型论依据。全部证明在 Coq 中形式化。
Abstract In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not always enjoy principal signatures. This observation is called the avoidance problem. In the past, the problem has been circumvented using a variety of devices for moving variables so they can remain in scope. These devices work, but have heretofore lacked a logical foundation. They have also lacked a presentation in which the dynamic semantics is given on the same phrases as the static semantics, which limits their applications. We can provide a best supersignature avoiding a variable by fiat, by adding an existential signature that is the least upper bound of its instances. This idea is old, but a workable metatheory has not previously been worked out. This work resolves the metatheoretic issues using ideas borrowed from focused logic. We show that the new theory results in a type discipline very similar to the aforementioned devices used in prior work. In passing, this gives a type-theoretic justification for the generative stamps used in the early days of the static semantics of ML modules. All the proofs are formalized in Coq.