Compositional Compiler Correctness for Scala

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