1 files changed, 26 insertions, 0 deletions
diff --git a/content/zettel/3a7b.md b/content/zettel/3a7b.md
new file mode 100644
index 0000000..e256c82
--- /dev/null
+++ b/content/zettel/3a7b.md
@@ -0,0 +1,26 @@
++++
+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} $$