The soundness of some transformations performed by compilers relies on semantic properties of the programs. In particular, aliasing information is needed to reason on memory accesses. Some properties can be established using analysis on low-level representations of programs, but an alternative is to propagate information available at higher levels. This latter approach involves a representation of information which is both exploited and maintained by the successive compilation passes. Justifying the correctness of the transformations then requires not only a precise semantics of the intermediate representations, but also a formalisation of the representation of information. We propose an intermediate representation that retains high-level information through expressive but statically checked dependent types. We encode non-aliasing information using memory fragments, whose implementation with a global memory is justified by a linearity criterion. We formalize in Rocq the intermediate representation, its semantics and some compilation passes. We also formalize for this purpose a generic functional SSA representation, which enables the definition of effectful languages.
Benjamin Bonneau (Wed,) studied this question.