一句话：提出一套逻辑框架，使约束式类型推断与elaboration能在Coq中模块化地机器验证其可靠性与完备性。
静态类型语言（如OCaml、Haskell）的类型推断通常分为约束生成与约束求解两个阶段，elaboration（为程序补充显式类型标注）也可如此组织。然而，现有机器验证的类型推断实现大多不采用这种阶段分离的约束式结构；少数采用者往往不可执行、缺少带效应的抽象，且不包含elaboration，导致实际实现与证明助手内的形式化之间存在鸿沟。本文提出一种方法，支持在存在elaboration时对单子式约束生成进行模块化推理：其中包括一个用于推理元变量的领域特定基础逻辑，以及一个可对约束含义进行抽象推理的程序逻辑。作者在Coq证明助手中机器化实现了该技术，并以带布尔值的简单类型λ演算为案例，对三个带elaboration的类型推断器验证了可靠性与完备性。这是首次表明类型推断算法可以按其实际实现形式——命令式风格、模块化分解为约束生成与求解、并向编译器后续阶段输出elaborated项——进行验证。
Type inference is essential for statically-typed languages such as OCaml and Haskell. It can be decomposed into two (possibly interleaved) phases: a generator converts programs to constraints; a solver decides whether a constraint is satisfiable. Elaboration, the task of decorating a program with explicit type annotations, can also be structured in this way. Unfortunately, most machine-checked implementations of type inference do not follow this phase-separated, constraint-based approach. Those that do are rarely executable, lack effectful abstractions, and do not include elaboration. To close the gap between common practice in real-world implementations and mechanizations inside proof assistants, we propose an approach that enables modular reasoning about monadic constraint generation in the presence of elaboration. Our approach includes a domain-specific base logic for reasoning about metavariables and a program logic that allows us to reason abstractly about the meaning of constraints. To evaluate it, we report on a machine-checked implementation of our techniques inside the Coq proof assistant. As a case study, we verify both soundness and completeness for three elaborating type inferencers for the simply typed λ -calculus with Booleans. Our results are the first demonstration that type inference algorithms can be verified in the same form as they are implemented in practice: in an imperative style, modularly decomposed into constraint generation and solving, and delivering elaborated terms to the remainder of the compiler chain.