SHF: SMALL: Intermediate Languages for Safe and Efficient Compilation

编译器验证的重要性是众所周知的，特别是对于高安全性和高保证的应用程序。不管我们对源代码有多自信，如果编译器引入了自己的错误和安全缺陷，那么再多的程序验证也无法在编译过程中幸存下来。 尽管经过验证的编译器在今天已经成为现实，但今天的编译器作者所采用的许多技术还没有成为正式的系统。 这破坏了对优化编译器的正确性证明的信心。 这项研究的智力价值是解决安全和效率问题的中间语言的设计和实现。 工作重点是格拉斯哥Haskell编译器。然而，开发并不局限于特定的语言，而是专注于更通用的框架。 更广泛的影响的研究包括改进的方法，验证编译;提供一个坚实的语义编译器的所有阶段，使验证更组合，使验证更复杂的编译器可行。该项目影响的不仅仅是中间语言，因为更广泛的经验教训可以融入源语言本身。这项工作代表了通过正式解决集成依赖类型和效果的困难挑战来扩展当前语言的证明能力的重要一步。例如，Haskell是一种纯函数式语言，但它的实现使用了涉及重新分配的memoization。充分表示实现技术的中间语言必须支持效果。使效果显式化不仅增加了对编译器正确性的信心，而且为优化提供了更多的机会，以产生更好的代码。虽然目前的研究集中在将高级功能推下编译管道，但这里的目标也是将低级功能拉上管道。在高级别和低级别之间找到正确的平衡是具有挑战性的，因为人们希望利用低级别的功能来提高效率，而不会破坏纯度的优势，最终阻碍而不是帮助优化。设计有用的中间语言的关键不在于程序必须是纯的，而在于它们使用良性的效果，即保证函数行为的效果。指导原则是在中间语言的设计和模型中保持与证明理论的紧密联系，特别是具有混合调用约定的中间语言。

The importance of compiler verification is well established, especially for high-security and high-assurance applications. Regardless of how confident we are in our source code, no amount of program verification can survive the compilation process if the compiler introduces its own bugs and security flaws. Even though verified compilers are a reality today, many of the techniques employed by today's compiler writers have not made it into a formal system. This undermines confidence in a correctness proof of an optimizing compiler. The intellectual merit of this research is the design and implementation of intermediate languages that address both safety and efficiency concerns. The work focuses on the Glasgow Haskell compiler. However, the development is not tied to a specific language but focuses on a more general framework. The broader impact of the research consists of improving the approaches to verified compilation; providing a solid semantics for all stages of the compiler makes verification more compositional and makes verifying more complex compilers feasible. The project impacts more than just intermediate languages, because the broader lessons learned can be incorporated into source languages themselves. The work represents an important step toward extending current languages with proving capabilities by formally addressing the difficult challenge of integrating dependent types and effects.Functional language implementations rely heavily on effects for efficiency. Haskell, for example, is a pure functional language but its implementation uses memoization that involves reassignment. Intermediate languages that adequately represent implementation techniques must support effects. Making effects explicit not only increases confidence in compiler correctness, but also presents more opportunities for optimizations to produce better code. Whereas current research has focused on pushing high-level features down the compilation pipeline, the goal here is to also pull low-level features up the pipeline. Finding the right balance between high and low levels is challenging, since one wants to exploit low-level features to enhance efficiency without ruining the advantages of purity and ultimately hindering more than helping optimizations. The key to design useful intermediate languages is not that programs are necessarily pure, but that they use benign effects, namely effects that guarantee functional behavior. The guiding principle is to keep a strong connection with proof theory in the design and models of intermediate languages, especially the ones with mixed calling conventions.