Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2404.18067 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909183817809920 |
|---|---|
| author | Jiang, Dongchen Fu, Chenxi |
| author_facet | Jiang, Dongchen Fu, Chenxi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_18067 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Type Inference for Isabelle2Cpp Jiang, Dongchen Fu, Chenxi Logic in Computer Science 68N30 D.2.4 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. |
| title | Type Inference for Isabelle2Cpp |
| topic | Logic in Computer Science 68N30 D.2.4 |
| url | https://arxiv.org/abs/2404.18067 |