Type Inference for Isabelle2Cpp

Applied Sciences 2026 Open access

Read full text
Authors: Dongchen Jiang, Yongkang Mao, Chenxi Fu
DOI: 10.3390/app16083828
Cited by: 0

Abstract

Isabelle2Cpp is a code generation framework that supports the automatic generation of C++ code from Isabelle/HOL specifications. However, when type information in an Isabelle/HOL specification is incomplete, Isabelle2Cpp may not be able to complete code generation automatically. To address this issue, this paper presents a type system for Isabelle2Cpp that performs type inference and type unification for expressions in its intermediate representation. The system introduces new type inference rules and unification algorithms to enhance the Isabelle2Cpp framework. By incorporating this type system, Isabelle2Cpp provides more comprehensive type information for expressions, leading to more complete and accurate C++ code generation.

Fields of Study & Subjects

Formal Methods in Verification

Publication details

Journal / source
Applied Sciences
Volume
16
Issue
8
Pages
3828–3828
Publication date
14 April 2026
Language
EN