From 89f851d4d73f347031db2b77aa87737757baafdb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 13 Sep 2021 09:38:39 +0100 Subject: Simplify title --- proof.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proof.tex b/proof.tex index e54a9af..a02baf9 100644 --- a/proof.tex +++ b/proof.tex @@ -1,6 +1,6 @@ -\section{Semantics Preservation Proof of Translation}\label{sec:proof} +\section{Correctness Proof}\label{sec:proof} -\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'} +%\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'} Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C-to-Verilog compilation. This section describes the main correctness theorem that was proven and the key ideas in the proof. The full Coq proof is available online~\cite{yann_herklotz_2021_5093839}. -- cgit