Type Inference for Isabelle2Cpp

TL;DR

This paper introduces a type inference system for Isabelle2Cpp, enhancing its ability to generate complete and accurate C++ code from Isabelle/HOL specifications by inferring missing type information.

Contribution

It proposes a novel type system with inference rules and unification algorithms to improve Isabelle2Cpp's code generation capabilities.

Findings

Enhanced type information leads to more complete code generation

New type inference rules improve accuracy of expression translation

Framework supports automatic type inference for Isabelle/HOL 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.