[ML'22] Do Mutable Variables Have Reference Types? скачать в хорошем качестве

[ML'22] Do Mutable Variables Have Reference Types?

Do Mutable Variables Have Reference Types? Oleg Kiselyov (Tohoku University, Japan) 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 solutions while avoiding any restrictions. The title question is the key.