Type Inference for Isabelle2Cpp
Dongchen Jiang, Chenxi Fu
TL;DR
This work addresses the challenge of incomplete type information in Isabelle/HOL that hinders automatic C++ code generation by Isabelle2Cpp. It introduces a Hindley-Milner–based type system with three cooperating modules—pattern parameter extraction, bottom-up type inference, and top-down type completion—to perform type inference and unification on the Isabelle2Cpp intermediate representation. The authors define expressions and types, establish a three-part inference framework with a unification mechanism, and implement a type solver Σ to track constructors and functions. Through a case study on binary search and product_lists, the approach yields explicit, strongly typed C++ code, reducing the need for decltype/auto and improving the completeness and correctness of generated code. The methodology enhances practical code generation from executable Isabelle/HOL specs and strengthens Isabelle2Cpp’s applicability to real-world specifications.
Abstract
Isabelle2Cpp is a code generation framework that supports automatic generation of C++ code from Isabelle/HOL specifications. However, if some type information of Isabelle/HOL specification is missing, Isabelle2Cpp may not complete the code generation automatically. In order to solve this problem, this paper provides a type system for Isabelle2Cpp, which is used to perform type inference and type unification for expressions of the intermediate representation in Isabelle2Cpp. The system introduces new type inference rules and unification algorithms to enhance the Isabelle2Cpp framework. By incorporating the type system, the Isabelle2Cpp framework can provide more comprehensive type information for expression generation, which leads to more complete and accurate C++ code.