Type Inference for Isabelle2Cpp
Source abstract
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.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Formal Methods in Verification
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
School of Information Science and Technology, Beijing Forestry University, Beijing 100083, China
References (17)
Show source-provided references
1. Nipkow, T., Wenzel, M., and Paulson, L.C. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Springer.10.1007/3-540-45949-9 ↗
2. Generation of C++ Code from Isabelle/HOL Specification10.1142/S0218194022500401 ↗
3. Type systems10.1145/234313.234418 ↗
4. Explaining type inference10.1016/0167-6423(95)00007-0 ↗
5. The system F of variable types, fifteen years later10.1016/0304-3975(86)90044-7 ↗
6. A theory of type polymorphism in programming10.1016/0022-0000(78)90014-4 ↗
7. Damas, L. (2015). Type Assignment in Programming Languages, The University of Edinburgh, Old College. KB Thesis Scanning Project.
8. Soosaipillai, H. (1990). An Explanation Based Polymorphic Type Checker for Standard ML. [Master’s Thesis, Heriot-Watt University].
9. Heeren, B.J., Hage, J., and Swierstra, S.D. (2002). Generalizing Hindley-Milner Type Inference Algorithms, Information and Computing Sciences, Utrecht University.
10. Principality and type inference for intersection types using expansion variables10.1016/j.tcs.2003.10.032 ↗
11. OutsideIn (X) Modular type inference with local assumptions10.1017/S0956796811000098 ↗
12. Traytel, D., Berghofer, S., and Nipkow, T. (2011). Extending Hindley-Milner type inference with coercive structural subtyping. Programming Languages and Systems: 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, 5–7 December 2011, Proceedings 9, Springer.
13. Object-oriented type inference10.1145/118014.117965 ↗
14. Local type inference10.1145/345099.345100 ↗
15. Chen, L., He, Z., and Mao, B. (2020). Cati: Context-assisted type inference from stripped binaries. 2020 50th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), IEEE.10.1109/DSN48063.2020.00028 ↗
16. Hellendoorn, V.J., Bird, C., Barr, E.T., and Allamanis, M. (2020). Deep learning type inference. Proceedings of the 2018 26th Acm Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Association for Computing Machinery (ACM).10.1145/3236024.3236051 ↗
17. Krauss, A. (2026, April 11). Defining Recursive Functions in Isabelle/HOL. Available online: https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1/doc/functions.pdf&ved=2ahUKEwiEgNyKg_yTAxWskq8BHR7xJBwQFnoECBwQAQ&usg=AOvVaw1_oYLdE5ure9Z4l3FSzA9H.