Compositional Compiler Correctness for Scala

点击翻译按钮获取中文摘要

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.