2022/11/08 by Oleg Kiselyov, Kiselyov, Oleg
Computer Science · #D.3.1 #D.3.3 #F.3.2 #F.3.3 #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2211.04107
openalex publication_date 2022/11/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Implicit heterogeneous metaprogramming (a.k.a. offshoring) is an attractive approach for generating C with some correctness guarantees: generate OCaml code, where the correctness guarantees are easier to establish, and then map that code to C. The key idea is that simple imperative OCaml code looks like a non-standard notation for C. Regretfully, it is false, when it comes to mutable variables. In the past, the approach was salvaged by imposing strong ad hoc restrictions. The present paper for the first time investigates the problem systematically and discovers general solutions needing no restrictions. In the process we explicate the subtleties of modeling mutable variables by values of reference types and arrive at an intuitively and formally clear correspondence. We also explain C assignment without resorting to L-values.