可变变量是否具有引用类型？
摘要：隐式异构元编程（即外包）是一种生成具有某些正确性保证的C代码的吸引人方法：生成OCaml代码，在那里正确性保证更容易建立，然后将该代码映射到C。关键思想是简单的命令式OCaml代码看起来像C的非标准符号。可惜的是，当涉及到可变变量时，这是错误的。过去，该方法通过施加强制性的特殊限制而被拯救。本文首次系统地研究了这个问题，并发现了不需要任何限制的通用解决方案。在这个过程中，我们阐明了使用引用类型的值来建模可变变量的微妙之处，并得出了一种直观和形式清晰的对应关系。我们还解释了C赋值而不借助L值。
作者：Oleg Kiselyov (Tohoku University, Japan)
论文ID：2211.04107
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-09