*Result*: Modular reasoning about combining modular compiler phases

*Compilers are large and complex pieces of software, which can be challenging to work with. Modularity has significant benefits in such cases: building a complex system from a series of simpler components can make understanding, maintaining, and reasoning about the resulting software more straightforward. Not only does this modularity aid the compiler developer, but the compiler user benefits too, from a compiler that is more likely to be correct and regularly updated. A good focus for modularity in a compiler lies in the phases that make up the compiler pipeline. Often, compiler phases involve transforming some graph structure, in order to perform program rewriting. Techniques for automatically combining such graph transformations aim to promote modularity whilst mitigating the increased performance overheads that can occur from an increased number of separate transformations. Nevertheless, it is important that the effectiveness and correctness of compiler phases is not compromised in favour of modularity or performance. Therefore, the combined graph transformations need to still satisfy the intended outcomes of their individual components. Many existing approaches either take an informal approach to soundness, or impose conditions that are too restrictive for the kind of graph transformations found in a realistic compiler. Some approaches only allow transformations to be combined if the ensuing transformation will produce identical results. However, certain compiler optimisations behave more effectively in combination, thus producing a different but better optimised result. Another limitation of some approaches is that, although the compiler phases are intentionally modular, the process of combining them is often tested or reasoned about in a non-modular way, once they have already been combined. Thus, this thesis outlines an approach for modular reasoning about successfully combining modular compiler phases, where success refers to preserving only the truly necessary behaviour of transformations. Focusing on postorder transformations of, first, abstract syntax trees and, then, program expression graphs, the fusion technique of interleaving transformations combines compiler phases, reducing the number of graph traversals required. Postconditions allow compiler developers to encode the behaviour required of a given compiler phase, with preservation of postconditions then a significant part of successful fusion. Building on these ideas, this thesis formalises the idea of postcondition preserving fusion, and presents criteria that are sufficient to facilitate modular reasoning about the success of fusion.*