Isabelle2Cpp是一个从Isabelle/HOL规范到C++程序的代码生成框架, 它使得人们能够将Isabelle/HOL规范形式化验证的方便性和C++程序的高效性相结合, 实现从验证过的Isabelle/HOL函数式规范到高效C++代码的自动正确转换. 针对代码生成框架在类型提取方面的欠缺, 本文为Isabelle2Cpp框架添加了类型推理系统, 用于完成对Isabelle2Cpp中间表示所有表达式的类型推理及类型实例化工作. 基于该系统的类型推理, Isabelle2Cpp框架能够获得更为完善的类型信息, 实现了对缺失类型信息Isabelle/HOL规范的C++代码自动生成.