The correctness of a compiler is naturally phrased as a problem of program equivalence: any source program should be equivalent to the
result of compiling it. We want this notion of equivalence to be compositional such that (1) we can verify a compiler in a modular
fashion, and (2) we can link modules separately compiled by one or several verified compilers without losing the correctness guarantee.
Unfortunately, existing methods do not support both. With the help of "parametric bisimulations", which we introduced last year, we hope to
change this.