From c3f04aee8d41069aded014f3e47e50037e03d4ce Mon Sep 17 00:00:00 2001
From: John Wickerson <j.wickerson@imperial.ac.uk>
Date: Thu, 4 Jun 2020 15:40:46 +0000
Subject: Update on Overleaf.

---
 main.tex | 33 ++++++++++++++++++++++++++-------
 1 file changed, 26 insertions(+), 7 deletions(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index 9547da2..4e4675e 100644
--- a/main.tex
+++ b/main.tex
@@ -18,8 +18,7 @@
 \acmNumber{CONF} % CONF = POPL or ICFP or OOPSLA
 \acmArticle{1}
 \acmYear{2018}
-\acmMonth{1}
-\acmDOI{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn}
+\acmMonth{1}\acmDOI{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn};'--
 \startPage{1}
 
 %% Copyright information
@@ -52,6 +51,13 @@
 \usepackage{mathpartir}
 \usepackage{subcaption}
 
+\newif\ifCOMMENTS
+\COMMENTStrue
+\newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
+\newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}}
+\newcommand\YH[1]{\Comment{green!50!black}{YH}{#1}}
+\newcommand\JP[1]{\Comment{blue!50!black}{JP}{#1}}
+
 \begin{document}
 
 %% Title information
@@ -97,7 +103,7 @@
 \author{James Pollard}
 %\authornote{with author1 note}          %% \authornote is optional;
                                         %% can be repeated if necessary
-\orcid{0000-0000-0000-0000}             %% \orcid is optional
+\orcid{0000-0003-1404-1527}             %% \orcid is optional
 \affiliation{
 %  \position{PhD Student}
 %  \department{Electrical and Electronic Engineering} %% \department is recommended
@@ -196,11 +202,24 @@ Definition of state.
   s = (\Gamma, \Delta)
 \end{equation}
 
-Definition of stmntrun.
+Definition of stmntrun. \JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.}
+
+\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things
+based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.}
+
+\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.}
+
+\begin{align}
+    \text{stmntrun}\ f\ s\ \mathtt{Vskip} &= s \\
+    \text{stmntrun}\ f\ s_0\ (\mathtt{Vseq}\ \mathit{st}_1\ \mathit{st}_2) &= \text{stmntrun}\ f\
+    (\text{stmntrun}\ f\ s_0\ \mathit{st}_1)\ \mathit{st}_2
+\end{align}
 
 \begin{equation}
   \label{eq:1}
-  \inferrule[Skip]{ }{\text{stmntrun}\ f\ s\ \mathtt{Vskip}\ s}
+  \inferrule[Skip]{ }{\text{stmntrun}\ f\ s\ \mathtt{Vskip} = s}
 \end{equation}
 
 \begin{equation}
@@ -230,7 +249,7 @@ Definition of stmntrun.
 
 \begin{equation}
   \label{eq:7}
-  \inferrule[CaseDefault]{\text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ \text{stmntrun}\ f\ s_{0}\ st\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
+  \inferrule[CaseDefault]{\text{stmntrun}\ f\ s_{0}\ st\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
 \end{equation}
 
 \begin{equation}
@@ -240,7 +259,7 @@ Definition of stmntrun.
 
 \begin{equation}
   \label{eq:9}
-  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
+  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
 \end{equation}
 
 %% Acknowledgments
-- 
cgit