一句话：用类型论部分 Galois 连接与反连接为依赖互操作性建立语义基础，并在 Coq 中机器验证。
全谱依赖类型有助于构造正确软件，但认证软件仍需与简单类型或无类型程序交互，例如系统调用或遗留库。依赖互操作性用运行时检查换取静态保证，使简单类型值可安全强制为依赖类型，反之亦可。本文给出依赖互操作性的语义基础，核心是类型等价与类型论部分 Galois 连接，以刻画类型间强制的部分性。部分 Galois 连接保证依赖类型到运行时检查的翻译对依赖类型不变式既健全又完备；反连接则给出更弱但更高效的健全检查。框架在 Coq 中构造性实现并机器验证。用户可定义领域特定部分连接，由库完成提升，从而在 Coq 内定制到可互操作 OCaml 程序的提取。
Abstract Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the dependent interoperability framework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this article, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notions of type-theoretic partial Galois connections as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an anticonnection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial connections between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.