Update on Overleaf.

2 files changed, 33 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index ced45f4..3ac94aa 100644
--- a/main.tex
+++ b/main.tex
@@ -193,6 +193,13 @@ Therefore, work is being done to prove the equivalence between the generated har
 
 \subsection{HLS}
 
+\JW{Some papers to cite somewhere:
+\begin{itemize}
+    \item \citet{kundu+08} have done translation validation on an HLS tool called SPARK.
+    \item \citet{chapman+92} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB: Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
+\end{itemize}
+}
+
 \section{Verilog Semantics}
 
 Definition of state.
@@ -209,7 +216,7 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.}
 
-\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now.  One more thing I noticed though is that recursive definitions will need an \texttt{option} type.}
+\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now.  One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.}
 
 \begin{align}
     \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\
diff --git a/references.bib b/references.bib
index 63a9f94..45c8419 100644
--- a/references.bib
+++ b/references.bib
@@ -83,3 +83,28 @@
   urldate         = {2020-06-06},
   year            = 2020,
 }
+
+@InProceedings{kundu+08,
+author="Kundu, Sudipta
+and Lerner, Sorin
+and Gupta, Rajesh",
+editor="Gupta, Aarti
+and Malik, Sharad",
+title="Validating High-Level Synthesis",
+booktitle="Computer Aided Verification (CAV)",
+year="2008",
+publisher="Springer",
+pages="459--472",
+}
+
+@INPROCEEDINGS {chapman+92,
+author = {Richard Chapman and Geoffrey Brown and Miriam Leeser},
+booktitle = {European Conference on Design Automation (EDAC)},
+title = {Verified high-level synthesis in BEDROC},
+year = {1992},
+pages = {59--63},
+doi = {10.1109/EDAC.1992.205894},
+url = {https://doi.ieeecomputersociety.org/10.1109/EDAC.1992.205894},
+publisher = {IEEE Computer Society},
+}
+