Isabelle2Cpp は Isabelle/HOL 仕様から C++ コードを自動生成するフレームワークですが、Isabelle/HOL 仕様に一部の型情報が欠落している場合、Isabelle2Cpp は自動的にコード生成を完了できません。本論文は、Isabelle2Cpp のための型システムを提供し、型推論と型統一を行うことで、より完全かつ正確な C++ コードの生成を可能にします。
