\lettrine[nindent=0ex]I{n} this work, I have spanned the arc from down-to-earth compiler transformations over formal semantics to machine-verified proofs of operational properties of the compiler transformation.

\medskip

By introducing the Call Arity analysis into the Haskell compiler GHC, I made it practically possible to let an important class of list-consuming and -processing functions take part in the list fusion program transformation, which is an important mechanism to make idiomatic Haskell code perform well. This solves a long-standing open issue.

My key observation was that in the context of a lazy programming language, a good arity analysis requires the help of a precise cardinality analysis, and my key contribution is the novel cardinality analysis based on the notion of co-call graphs, which allows the compiler to get precise information about how often a variable is used, even if the call occurs from within a recursive function.

Empirical measurements show that introducing the analysis improves the performance of some programs in the standard benchmark suite. Furthermore, changing the definitions of list consumers with accumulators to now take part in list fusion provides a more significant performance boost to a number of existing programs, and a huge improvement to some programs. Thus it now allows performance-aware programmers to write more high-level code, instead of manually transforming their code \pagebreak[4] into a less idiomatic form to make up for the compiler’s previous inability to produce good code in these situations.

One can consider Call Arity to be a whole-program analysis, given that it works best if all occurrences of a function are known. I have shown that a compiler employing separate compilation can still make good use of such a transformation, as inlining in some cases gives the analysis the chance to see all use-sites of a function’s definition.

\medskip

To pave the way to a formal treatment of such analyses and transformations of lazy functional programs, I created a formalisation of Launchbury’s natural semantics, of Sestoft’s mark-1 abstract machine and of related denotational semantics in the interactive theorem prover Isabelle. These reusable artefacts extend the growing library of formalisations and lower the barrier of entry for formalising further research on programming languages in a machine-checked setting.

The formalisation contains a proof of the adequacy of Launchbury’s natural semantics with regard to a standard denotational semantics. The original paper only sketches this proof, and the sketch has so far resisted attempts to complete it with rigour. By slightly deviating from the path outlined in the proof sketch, I found a more elegant and more direct proof of adequacy, which is also machine-checked. This does not shake the foundations a large swathes of research, as the adequacy theorem holds as expected, but it fortifies them instead.

My formalisation builds on relatively new mechanisms for dealing with names and binders in Isabelle, namely the Isabelle package Nominal2, and constitutes one of the largest developments using this technology. It is also the first to combine it with domain theory in the form of the HOLCF package.

\medskip

Finally, I used these formalised semantics to model the Call Arity analysis and transformation and proved not only functional correctness, but also -- and especially -- safety: The performance of the program is not reduced by applying the Call Arity transformation.


I chose to measure performance by counting the number of dynamic allocations, and I explain why this measure is suitable to ensure that the Call Arity analysis does not go wrong, and that it is a good compromise between formal tractability and “real” performance.

I introduced the notion of trace trees as a suitable abstract type to think and reason about cardinality analyses.
%
My proof is modularised using Isabelle’s \emph{locales}, making it possible to re-use just parts of it.
%
This should make similar formalisation endeavours, such as a safety proof of the other arity and cardinality related analyses in GHC, more tractable.

As with most formalisation attempts, by pursuing it I have improved the understanding of how and why the analysis works, sharpened its specification and rooted out bugs that the conventional test suite did not find.

Operational properties of compiler transformations, such as safety, are rarely investigated on a formal level, especially not with the rigour provided by a theorem prover. I have demonstrated that such a feat is possible, with an effort that may be justified in certain high-stake use cases.


There are limits to the applicability of my safety theorem, as Call Arity is but one step in a large sequence of other analyses and transformations performed by the compiler. Therefore, the no-regression result does not transfer to the complete compiler in complete universality: For example, if subsequent transformations were not monotonous, then the introduction of Call Arity could have an overall negative effect on some programs.
%Furthermore, modern computer architectures are sensitive to seeminly arbitrary changes to the code structure
I elaborate on this and other aspects of the “formalisation gap” immanent in such formal work.

To overcome some of the formalisation gap, it would be desirable to formalise GHC's Core in Isabelle. Using Isabelle's code generation to Haskell and GHC’s plugin architecture, even verified implementations of Core-to-Core transformations in GHC would appear to be within reach. This would be a milestone on the way to formally verified compilation of Real-World-Haskell.


\medskip

All in all, this thesis exhibits an approach to the design and development of compiler transformations that is supported by formal methods. I hope that it will inspire more researchers in this field to dare to not only test their claims, but actually prove them, and to even do that with the rigour provided by machine-checked proofs.