构造性Galois连接：驯服用于机械化元理论的Galois连接框架

Galois连接是语义学中构建抽象的基础工具，其使用位于抽象解释理论的核心。然而，Galois连接的机械化仍局限于受限的使用模式，阻碍了它们在机械化元理论与认证编程中的普遍应用。本文提出构造性Galois连接（constructive Galois connections），其为Galois连接的一种变体，在纸笔证明与证明助手中均有效；相对于经典Galois连接的很大子集是完备的；并支持更通用的推理原则，包括Cousot所倡导的“计算式（calculational）”风格。为设计构造性Galois连接，我们识别出经典连接的一种受限使用模式，该模式既通用又易于在依赖类型函数式编程语言中机械化。我们元理论的关键在于向Galois连接添加单子结构以控制一种“规约效应（specification effect）”。有效应计算可进行经典推理，而纯计算具有可抽取的计算内容。我们的元理论使得在规约与实现世界间显式移动成为可能。为验证我们的方法，我们提供了两个将文献中已有证明机械化的案例研究：其一使用计算式抽象解释设计静态分析器，另一为渐进类型化形成语义基础。两个机械化证明均紧密遵循其原始纸笔对应物，采用了先前机械化方法未涵盖的推理原则，支持抽取已验证算法，且均为新颖工作。