Refined Environment Classifiers: Type- and Scope-safe Code Generation with Mutable Cells
Refined Environment Classifiers: Type- and Scope-safe Code Generation with Mutable Cells
复制标题
细化环境分类器：使用可变单元生成类型和范围安全的代码
DOI：
10.1007/978-3-319-47958-3_15
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Yuto Sudo
中科院分区：
文献类型：
--
作者：
Oleg Kiselyov;Yukiyoshi Kameyama;Yuto Sudo
生成高性能代码并在循环和函数体中应用典型优化涉及移动或存储开放代码以供以后使用，通常是在不同的绑定环境中。变量有足够的机会未绑定或意外捕获。这一直是一个坚韧的挑战，静态地确保通过建设所生成的代码仍然是良好的类型和良好的范围：所有自由变量的操纵和存储的代码片段最终应绑定，由他们的预期binders.We提出的演算代码生成的可变状态，第一次实现类型安全和卫生没有特别的限制。微积分非常类似于基于区域的内存管理，但数量级更简单的证明。它采用了对自由变量的正确抽象表示，像自然演绎中的假设一样，自由变量不受类型环境或编号约定所强加的官僚主义语法的约束。尽管演算是为了形式化而设计的，并且故意是最基本的，但它很容易实现，并且对于编写实际的程序来说并不太麻烦。
Generating high-performance code and applying typical optimizations within the bodies of loops and functions involves moving or storing open code for later use, often in a different binding environment. There are ample opportunities for variables being left unbound or accidentally captured. It has been a tough challenge to statically ensure that by construction the generated code is nevertheless well-typed andwell-scoped: all free variables in manipulated and stored code fragments shall eventually be bound, by their intended binders.We present the calculus for code generation with mutable state that for the first time achieves type-safety and hygiene without ad hoc restrictions. The calculus strongly resembles region-based memory management, but with the orders of magnitude simpler proofs. It employs the rightly abstract representation for free variables, which, like hypothesis in natural deduction, are free from the bureaucracy of syntax imposed by the type environment or numbering conventions.Although the calculus was designed for the sake of formalization and is deliberately bare-bone, it turns out easily implementable and not too bothersome for writing realistic program.