+++
title = "Correctness argument for translation validation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a7a"]
forwardlinks = ["3a7c"]
zettelid = "3a7b"
+++

Why is translation validation correct?

If you have two languages $S$ and $T$ that you are translating in
between, you are first going to evaluate both languages using abstract
evaluation. This is a translation to a third intermediate language that
consists of a forest of registers $\mathcal{A}$.

The first step in the correctness of the translation from the input
language $S$ to $\mathcal{A}$ is semantics preserving. This can be done
because semantics have to be defined for the abstract interpretation.

Then, using the same semantics for $\mathcal{A}$, one can prove that the
translation from $T$ to $\mathcal{A}$ is also semantics preserving. Then
one can prove the following:

$$ \frac{s : S \rightarrow_s \alpha : \mathcal{A} \quad t : T \rightarrow_t\alpha' : \mathcal{A} \quad \alpha \sim \alpha'}{s \sim t} $$