Compilers, which translate high-level source code written by programmers intothe low-level target code that runs on machines, play a critical role in theproduction of software. As such, they should be correct, i.e., they shouldpreserve the behavior of all programs they compile. Prior to this project, whilethere had been remarkable progress on formally verified compilers forincreasingly realistic languages, these verified compilers suffered from aserious limitation: they were proved correct under impractical assumptions aboutwhat the compiled code would be linked with, from no linking at all to linkingonly with code compiled from the same source language. These assumptions do notmatch reality as most software systems today are comprised of components writtenin different languages compiled by different compilers to a common target, aswell as low-level libraries that may be handwritten in the target language.
A central goal of this project was to investigate proof methods for buildingverified compositional compilers, which guarantee correct compilation ofcomponents, not just whole programs, and formally support linking with arbitrarytarget code.  The long-term vision, extending beyond this project, is to haveverified compositional compilers from languages as different as C, OCaml, Rust,and Coq to a common low-level target language that supports safeinteroperability between more precisely typed, less precisely typed, andtype-unsafe components. 
The first major result of this project was the development of a genericcompositional compiler correctness (CCC) theorem that we argue is the desiredtheorem when compiling components instead of whole programs. This resultaddresses a critical question: how do we even state the compiler correctnesstheorem in the presence of linking? While there have been a number of recentresults on compositional compiler correctness, they all state theircorrect-component-compilation theorems in remarkably different ways, yieldingpros and cons that aren't well understood.  We showed that specificcompiler-verification efforts can use their choice of formalism ``under thehood'' and then prove that their theorems imply CCC. 
The second major outcome of the project were compositional compiler correctnessresults for compilers that, unlike prior work, support linking withtarget-language features that are not present in the source language:specifically with control effects such as exceptions and call/cc. Linking withfeatures not present in the source is a critical feature since that often whyprogrammers implement components in different languages. 
The third major result of the project was a multi-language that supports safemixing of a high-level typed functional language with low-level assembly code.This is nontrivial since assembly is not compositional: assembly languagecomponents may be comprised of different numbers of basic blocks so it isn'tclear how to identify component boundaries. To support safe mixing, we designeda compositional typed assembly language (TAL), showed how to designmulti-language semantics so TAL components can be safely embedded in ahigh-level functional language and vice versa. 
The fourth major outcome of this project is a methodology for verifying thesoundness of foreign-function interfaces (FFIs).  Every language implements anFFI for language interoperability, but existing FFIs are all ad hoc. Wedeveloped a semantic framework for proving soundness of  FFIs as they are designed "in the wild", by which we mean that FFI developersimplement conversion between types of data from two different source languagesby implementing target-level conversion functions to mediate between datarepresentations coming from the two source languages. We applied thisframework to a series of case studies that demonstrate how this  approach allows us to account for complex differences in language semantics andmake efficiency trade-offs based on specifics of compilers or targets. 
The fifth major set of results pertain to compilation of languages with advancedtype systems, specifically dependent types. Dependently typed languages such asthat of the Coq proof assistant have rich types that enable verification of fullfunctional correctness during program development.  This project showed how todevelop correct and *typed* compiler passes for the core language of the Coqproof assistant. These passes include typed CPS translation, which since 2002was conjectured to be impossible, typed closure conversion, and ANF. Theseresults are key to building a practical verified compiler for Coq which wouldensure that fully verified source code cannot be compromised via compiler bugsor unsafe linking.
The sixth major series of results from this project pertain to gradualtyping, i.e., the mixing of more precisely typed and less precisely typedcode. One of the goals of the project was to design a gradually type-safelow-level language that supports safe interoperability between components thatare statically type-safe (e.g., compiled from OCaml or Rust) and dynamicallytype-safe (e.g., compiled from Python or Scheme). This project produced a seriesof foundational results on design principles for gradually typed langauges. 
Finally, for education and broader impacts: the project involved development ofsummer school lectures delivered in 4 separate years at the Oregon PL Summer School  (OPLSS) on a variety of research results from this project. It also includedlectures and talks at ECOOP, the PL Mentoring Workshop, a keynote at theStrangeLoop conference, and courses at Northeastern that explain how ideas fromtype systems, runtime contract checking, gradual typing, multi-languagesemantics, and compiler correctness can be brought together to build verifiedcompilers for a multi-language world. 

Last Modified: 07/28/2023
Modified by: Amal Ahmed