Compositional Compiler Correctness for Scala

编译器的正确性通常是开发有效、可靠软件的一个重要因素。与初始源代码行为不同的目标代码是无用的，并且可能产生危险的后果。此外，编译器错误很难定位和修复，通常需要进行大量的测试。许多编译器验证工作倾向于关注整个程序的编译。然而，在现实中，经常需要编译与其他目标代码链接的组件。因此，在与尽可能多的组件进行链接时，能够保持正确性保证是有益的。这包括从不同的源语言编译的目标代码。语言互操作性是各种平台的关键特性。例如，一系列语言被编译成Java字节码并在Java虚拟机（JVM）上运行。由于有共同的编译目标，开发人员可以很容易地组合用这些语言编写的组件。Scala是一种越来越流行的JVM语言，它结合了函数式和面向对象的编程范式。它最初的目标之一是鼓励基于组件的软件开发。它与Java的强大互操作性在它的成功中发挥了很大的作用。Scala已经被集成到各个领域，包括科学计算、大数据和生物信息学。这些Scala应用程序中的大多数都需要与来自不同源的代码链接，无论是Java还是C或c++。因此，经过验证的Scala编译器需要在这些情况下保持保证。组合正确的编译侧重于在两个方向上传播正确性保证。水平组合确保在链接目标代码时保持保证。同时，垂直组合为多阶段编译器保留了保证。作为一种促进互操作性和模块化开发的高级语言，Scala将从这两个考虑因素中受益。目的与目的本研究旨在发展经过验证的组合编译技术。Perconti和Ahmed（2014）表明，通过发展跨语言关系，开发多语言语义可以促进组合正确的编译。这允许程序员用任意目标代码表达对链接的期望。可以在语言之间开发类型翻译，以便在链接时检查和保留保证。因此，我们的目标是将这种方法应用于Scala，作为一种流行的JVM语言。DOT是Scala的核心演算，体现了Scala的重要特性，并构成了其未来编译器开发的基础。这将在我们的工作中用作Scala的近似。我们将在DOT和Java字节码之间开发一系列翻译和中间语言，根据需要丰富字节码类型系统。我们将开发一种嵌入DOT、字节码和中间语言的多语言语义。这将通过一系列边界和类型转换指定这些语言之间的互操作性。我们将在这种多语言上定义一个等价关系，该等价关系可用于定义编译器正确性保证。我们将使用Coq来证明编译器是正确的，并且正确性保证按预期组合。新颖性和与EPSRC战略和研究领域的一致性ascala是一种日益流行的语言，在鼓励基于组件的软件中广泛使用JVM。因此，它将受益于当前对组合编译器正确性的关注。该研究属于EPSRC的两个主题：编程语言和编译器，以及验证和正确性。

Compiler correctness is often an important factor in the development of effective and reliable software. Target code which behaves differently to the initial source code is not useful, and can have dangerous consequences. Furthermore, compiler bugs can be difficult to locate and fix, often requiring extensive testing. Many compiler verification efforts tend to focus on whole-program compilation. However, in reality, it is often necessary to compile components which link with other target code. Hence, it is beneficial to be able to preserve correctness guarantees when linking with as wide a range of components as possible. This includes target code which has been compiled from different source languages.There are various platforms for which language interoperability is a key feature. For instance, a range of languages compile to Java bytecode and run on the Java Virtual Machine (JVM). As a result of the common compilation target, developers can easily combine components written in these languages. Scala is an increasingly popular JVM language, uniting functional and object-oriented programming paradigms. One of its initial aims was to encourage component based software development. Its strong interoperability with Java has played a large part in its success. Scala has been integrated into various fields, including scientific computing, big data and bioinformatics. The majority of these Scala applications require linking with code from different sources, be that Java or even C or C++. Hence, a verified Scala compiler would need to preserve guarantees in these cases.Compositionally correct compilation focusses on propagating correctness guarantees in two directions. Horizontal composition ensures that guarantees are maintained when linking target code. Meanwhile, vertical composition preserves guarantees for multi-phase compilers. As a high-level language which promotes interoperability and modular development, Scala stands to benefit from both of these considerations.Aims and objectivesThis research aims to develop verified compositional compilation techniques. As shown by Perconti and Ahmed (2014), developing a multi-language semantics can facilitate compositionally correct compilation, through the development of cross-language relations. This allows the programmer to express expectations about links with arbitrary target code. Type translations can be developed between the languages to check and preserve guarantees when linking. Hence, we aim to apply this approach to Scala, as an example of a popular JVM language.1. DOT is a core calculus for Scala, embodying its significant features and forming the basis of its future compiler development. This will be used as an approximation of Scala in our work. We will develop a series of translations and intermediate languages between DOT and Java bytecode, enriching the bytecode type system as necessary.2. We will develop a multi-language semantics which embeds DOT, bytecode and the intermediate languages. This will specify the interoperability between these languages through a series of boundaries and type translations. We will define an equivalence relation on this multi-language, which can be used to define the compiler correctness guarantees.3. We will use Coq to prove that the compiler is correct and that the correctness guarantees compose as desired.Novelty and alignment to EPSRC's strategies and research areasScala is an increasingly popular language, making wide use of the JVM in encouraging component based software. Therefore, it stands to benefit from the current interest in compositional compiler correctness.The research falls under the two EPSRC themes of Programming Languages and Compilers, and Verification and Correctness.