+++
title = "Proving compiler optimisations"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a7"]
forwardlinks = ["3a7b"]
zettelid = "3a7a"
+++

\[1\]

-   Module for general Analysis information
-   Use Kildall's algorithm to get information about what the compiler
    knows at that instruction
-   Algorithm is implemented generally in Module AnalysisEntries (AE)
-   Module for general transformations (Transfer)
-   Implement transformations based on module TransferEntries, which can
    prove other properties about the transformation for you
-   Transformations are then done by applying a functor which takes
    TransferEntries and returns the Transfer module.

<div id="refs" class="references csl-bib-body" markdown="1">

<div id="ref-bertot06_struc_approac_provin_compil_optim"
class="csl-entry" markdown="1">

<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">Y. Bertot, B. Grégoire, and X.
Leroy, “A structured approach to proving compiler optimizations based on
dataflow analysis,” in *Types for proofs and programs*, J.-C. Filliâtre,
C. Paulin-Mohring, and B. Werner, Eds., Berlin, Heidelberg: Springer
Berlin Heidelberg, 2006, pp. 66–81.</span>

</div>

</div>