.png){kind=icon}
Return
Type Inference for Isabelle2Cpp
.png){kind=icon}
PRE
AI
DOI：10.3390/app16083828.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Isabelle2Cpp
type inference
type system
code generation
Journal
A
IF:
2.5
Papers:
7.6K
Citations:
4
Organization
Cited Papers
.png){kind=icon}
ShareSave
ShareSaveShareSaveShareSaveShareSave
View more