该论文提出了一种名为 ILA（Intermediate Language for FHE）的中间语言和类型系统，用于确保全同态加密（FHE）程序的正确性。FHE 允许在密文上进行任意计算，但现有 FHE 编译器容易引入错误，例如密文噪声管理不当或运算类型不匹配。作者设计了一个类型检查框架，该框架在类型层面编码了密文的安全参数（如噪声预算、乘法深度等），使得类型安全的程序能够保证在解密后得到正确结果。具体而言，ILA 的类型系统包含依赖类型，可以跟踪每个值的噪声增长，并在编译时拒绝可能超出噪声阈值的操作。此外，论文还形式化了类型系统的正确性定理，证明类型良好的程序不会产生解密失败的输出。实验评估使用多个经典 FHE 应用（如线性回归、神经网络推理）来验证类型系统的有效性，结果显示 ILA 能够捕获多种常见的错误，且类型检查的开销在可接受范围内。该研究属于密码学与编程语言的交叉领域，为构建更可靠的 FHE 编译器提供了理论基础。