p_{n}.e_{n}\\}\right)\mapsto[B][\vec{v}/\vec{x}]e_{i}$.

Therefore, since extensional equivalence is closed under evaluation:

$[\vec{v}/\vec{x}](\texttt{case}\ e\ \\{p_{1}.e_{1}\mid\ldots\mid
p_{n}.e_{n}\\}\cong e^{\prime}:\tau)$

  * •

$\textsc{Iso}_{\text{case2}}$: By symmetry and $\textsc{Iso}_{\text{casel}}$.

  * •

$\textsc{Iso}_{\text{case3}}$ Let $\Gamma=\vec{y}:\vec{\tau}$ and let
$\vec{v}$ be arbitrary where $v_{i}:\tau_{i}$ and $v_{i}\ \mathsf{val}$ for
all $v_{i}\in\vec{v}$. Assume
$[\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime},x:\tau^{\prime},\Gamma^{\prime\prime}}.\sigma\land\sigma^{\prime}\right)$.
It must be shown that $[\vec{v}/\vec{y}](\texttt{case}\ e\
\\{\ldots\\}\cong\texttt{case}\ e^{\prime}\ \\{\ldots\\})$.

By the inductive hypothesis we have

$\overset{\mathsf{val}}{\forall}_{\Gamma}.\left(\text{if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$ then
$e\cong e^{\prime}$}\right)$

and therefore

$\left(\text{if
$[\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$
then $[\vec{v}/\vec{y}](e\cong e^{\prime})$}\right)$

Since $[\vec{v}/\vec{y}]\sigma$ only contains variables in $\Gamma^{\prime}$,
by assumption and conjunction we already have
$[\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$.
Therefore we may conclude $[\vec{v}/\vec{y}](e\cong e^{\prime})$.

Since we are only concerned with proving our approach sound over valuable
expressions, without loss of generality, we can assume that
$[\vec{v}/\vec{y}]e\Mapsto w$ for some value $w$ such that $\Gamma\vdash
w:\tau^{\prime}$ and $w\ \mathsf{val}$. By the inductive hypothesis we have

$\overset{\mathsf{val}}{\forall}_{\Gamma,x:\tau^{\prime}}.\left(\text{if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime\prime}}.\sigma^{\prime}\right)$
then $\texttt{case}\ x\ \\{\ldots\\}\cong\texttt{case}\ x\
\\{\ldots^{\prime}\\}$}\right)$

and therefore, since $x$ is fresh,

$\overset{\mathsf{val}}{\forall}_{x:\tau^{\prime}}.\left(\text{if
$[\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime\prime}}.\sigma^{\prime}\right)$
then $[\vec{v}/\vec{y}](\texttt{case}\ x\ \\{\ldots\\}\cong\texttt{case}\ x\
\\{\ldots^{\prime}\\})$}\right)$

Invoking this with $w$, we have

if
$[w/x][\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime\prime}}.\sigma^{\prime}\right)$
then $[\vec{v}/\vec{y}](\texttt{case}\ w\ \\{\ldots\\}\cong\texttt{case}\ w\
\\{\ldots^{\prime}\\})$

By assumption and conjunction we already have
$[w/x][\vec{v}/\vec{y}]\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime\prime}}.\sigma^{\prime}\right)$.
Therefore we may conclude

$[\vec{v}/\vec{y}](\texttt{case}\ w\ \\{\ldots\\}\cong\texttt{case}\ w\
\\{\ldots^{\prime}\\})$

Since $[\vec{v}/\vec{y}]e\cong w$ and
$[\vec{v}/\vec{y}]e\cong[\vec{v}/\vec{y}]e^{\prime}$, we have
$[\vec{v}/\vec{y}]e^{\prime}\cong w$ by transitivity. Then, by referential
transparency and the above equivalence, we have:

$[\vec{v}/\vec{y}](\texttt{case}\ e\ \\{\ldots\\}\cong\texttt{case}\
e^{\prime}\ \\{\ldots^{\prime}\\})$

  * •

$\textsc{Iso}_{\text{case4}}$ : Let $\Gamma=\vec{y}:\vec{\tau}$ and let
$\vec{v}$ be arbitrary where $v_{i}:\tau_{i}$ and $v_{i}\ \mathsf{val}$ for
all $v_{i}\in\vec{v}$. Assume
$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.\Psi$.
It must be shown that $[\vec{v}/\vec{y}](\texttt{case}\ x\
\\{M\\}\cong\texttt{case}\ x\ \\{M^{\prime}\\}:\tau)$.

Since extensional equivalence is defined only over closed expressions, without
loss of generality, we can assume that $[\vec{v}/\vec{y}]$ includes some
binding for $x$ $[v/x]$. By partial application,
$[\vec{v}/\vec{y}](\texttt{case}\ x\ \\{M\\}\cong\texttt{case}\ x\
\\{M^{\prime}\\}:\tau)$ is equivalent to $[\vec{v}/\vec{y}](\texttt{case}\ v\
\\{M\\}\cong\texttt{case}\ v\ \\{M^{\prime}\\}:\tau)$.

By Lemma A, $[\vec{v}/\vec{y}](\texttt{case}\ v\ \\{M\\}\cong\texttt{case}\ v\
\\{p_{1}.e_{1}\mid\ldots\mid p_{n}.e_{n}\\})$ and
$[\vec{v}/\vec{y}](\texttt{case}\ v\ \\{M^{\prime}\\}\cong\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\})$. So to show
$[\vec{v}/\vec{y}](\texttt{case}\ v\ \\{M\\}\cong\texttt{case}\ v\
\\{M^{\prime}\\}:\tau)$, it suffices to show $[\vec{v}/\vec{y}](\texttt{case}\
v\ \\{p_{1}.e_{1}\mid\ldots\mid p_{n}.e_{n}\\}\cong\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau)$.

Since case expressions are enforced to be exhaustive, there must be some
$p_{i}$ and $p_{j}^{\prime}$ such that $v\sslash p_{i}\dashv B$ and for all
$j<i$, $v\mathbin{\setminus\mkern-10.0mu\sslash}p_{j}$. Since $i\leq s$ or
$i>s$, we must consider both cases.

We first consider the case where $i\leq s$.

By our assumption that $[\vec{v}/\vec{y}]\Psi$ is valid and the semantics of
conjunction, we have that

$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.(\land_{i\in[s]}\sigma_{i})$

so in particular, at the $i$ such that $v\sslash p_{i}\dashv B$, we have

$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.\sigma_{i}$

Since $\sigma_{i}$ only contains variables from $\Gamma,\Gamma_{i},$ and
$\Gamma_{i}^{\prime}$, this is equivalent to
$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{i},\Gamma_{i}^{\prime}}.\sigma_{i}$.
Then, by our inductive hypothesis,
$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{i}}.(e_{i}\cong
e_{i}^{\prime})$. This implies $[\vec{v}/\vec{y}][B](e_{i}\cong
e_{i}^{\prime})$. Since $i\leq s$, by Lemma A, $v\sslash p_{i}\dashv B$,
$v\sslash p_{i}^{\prime}\dashv B$, and for all $j<i$,
$v\mathbin{\setminus\mkern-10.0mu\sslash}p_{j}$ and
$v\mathbin{\setminus\mkern-10.0mu\sslash}p_{j}^{\prime}$. So by
$\textsc{Dyn}_{\text{\ref{dyn:case2}}}$, $[\vec{v}/\vec{y}](\texttt{case}\ v\
\\{p_{1}.e_{1}\mid\ldots\mid p_{n}.e_{n}\\})\mapsto[\vec{v}/\vec{y}][B]e_{i}$
and $[\vec{v}/\vec{y}](\texttt{case}\ v\
\\{p_{1}^{\prime}.e_{1}^{\prime}\mid\ldots\mid
p_{m}^{\prime}.e_{m}^{\prime}\\})\mapsto[\vec{v}/\vec{y}][B]e_{i}^{\prime}$.
Since extensional equivalence is closed under evaluation, this implies
$[\vec{v}/\vec{y}](\texttt{case}\ v\ \\{p_{1}.e_{1}\mid\ldots\mid
p_{n}.e_{n}\\}\cong\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau)$ as desired.

This leaves the case where $i>s$. By our assumption that
$[\vec{v}/\vec{y}]\Psi$ is valid and the semantics of conjunction, we have
that
$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.(\land_{j\in[s+1,n]}((\land_{k\in[j-1]}(x\not\equiv
p_{k}))\land x\equiv p_{j})\Rightarrow\sigma_{j})$, so in particular, when
$j=i$ such that $v\sslash p_{i}\dashv B$, we have:

$[\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}(x\not\equiv
p_{k}))\land x\equiv p_{i})\Rightarrow\sigma_{i}$

Since $\Gamma$ is disjoint with all other listed contexts, this is equivalent
to:

$\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}[\vec{v}/\vec{y}](x\not\equiv
p_{k}))\land[\vec{v}/\vec{y}](x\equiv
p_{i}))\Rightarrow[\vec{v}/\vec{y}]\sigma_{i}$

Since $p_{i}$ and $p_{k}$ only contain variables in $\Gamma_{i}$ and
$\Gamma_{k}$ (and therefore, none of $\vec{y}$), we have:

$\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}[\vec{v}/\vec{y}]x\not\equiv
p_{k})\land[\vec{v}/\vec{y}]x\equiv
p_{i})\Rightarrow[\vec{v}/\vec{y}]\sigma_{i}$

Recalling that $[v/x]$ is included in $[\vec{v}/\vec{y}]$, this is equivalent
to:

$\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}v\not\equiv
p_{k})\land v\equiv p_{i})\Rightarrow[\vec{v}/\vec{y}]\sigma_{i}$

We may partially invoke this result with $B$ which gives us:

$[B]\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}v\not\equiv
p_{k})\land v\equiv p_{i})\Rightarrow[\vec{v}/\vec{y}]\sigma_{i}$

Since the list of contexts is pairwise disjoint and since neither $v$ nor
$p_{k}$ for any $k<i$ contain any variables in $\Gamma_{i}$, we can rearrange
this to get:

$\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.((\land_{k\in[i-1]}v\not\equiv
p_{k})\land v\equiv[B]p_{i})\Rightarrow[B][\vec{v}/\vec{y}]\sigma_{i}$

By Lemma A $v\equiv[B]p_{i}$ is true and by $i-1$ applications of Lemma A
$\land_{k\in[i-1]}v\not\equiv p_{k}$ is true, so this is equivalent to:

$\overset{\mathsf{val}}{\forall}_{\Gamma_{1},\Gamma_{1}^{\prime}\ldots\Gamma_{n},\Gamma_{n}^{\prime}}.[B][\vec{v}/\vec{y}]\sigma_{i}$

$\sigma$ only contains variables from $\Gamma,\Gamma_{i},$ and
$\Gamma_{i}^{\prime}$. Therefore, $[\vec{v}/\vec{y}]\sigma_{i}$ only contains
variables from $\Gamma_{i}$ and $\Gamma_{i}^{\prime}$. Therefore,
$[B][\vec{v}/\vec{y}]\sigma_{i}$ only contains variables from
$\Gamma_{i}^{\prime}$. Because of this, we can simplify and rearrange the
above to:

$[B][\vec{v}/\vec{y}]\overset{\mathsf{val}}{\forall}_{\Gamma_{i}^{\prime}}.\sigma_{i}$

This allows us to invoke the inductive hypothesis to get

$[B][\vec{v}/\vec{y}]e_{i}\cong[B][\vec{v}/\vec{y}]\texttt{case}\ x\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau$

Since the variables in $B$ don’t appear in $\texttt{case}\ x\
\\{M^{\prime}\\}$, and since $[v/x]$ is included in $[\vec{v}/\vec{y}]$, this
is equivalent to

$[B][\vec{v}/\vec{y}]e_{i}\cong[\vec{v}/\vec{y}]\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau$

By $\textsc{Dyn}_{\text{\ref{dyn:case2}}}$, $\texttt{case}\ v\
\\{p_{1}.e_{1}\mid\ldots\mid p_{n}.e_{n}\\}\mapsto[B][\vec{v}/\vec{y}]e_{i}$.

Therefore, since extensional equivalence is closed under evaluation:

$[\vec{v}/\vec{x}](\texttt{case}\ v\ \\{p_{1}.e_{1}\mid\ldots\mid
p_{n}.e_{n}\\}\cong\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau)$

So regardless of whether $i\leq s$ or $i>s$, we have
$[\vec{v}/\vec{x}](\texttt{case}\ v\ \\{p_{1}.e_{1}\mid\ldots\mid
p_{n}.e_{n}\\}\cong\texttt{case}\ v\
\\{p^{\prime}_{1}.e^{\prime}_{1}\mid\ldots\mid
p^{\prime}_{m}.e^{\prime}_{m}\\}:\tau)$ as desired

  * •

$\textsc{Iso}_{\text{case5}}$ : By symmetry and $\textsc{Iso}_{\text{case4}}$
.

We have verified the soundness of each rule. Therefore, by induction:

  * •

If $\Gamma\vdash e_{1}\ext@arrow
9999{\arrowfill@\Leftarrow\Relbar\Rightarrow}{}{\sigma}e_{2}:\tau\dashv\Gamma^{\prime}$
then $\overset{\mathsf{val}}{\forall}_{\Gamma}.\left(\text{if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$ then
$e_{1}\cong e_{2}:\tau$}\right)$.

  * •

If $\Gamma\vdash e_{1}\ext@arrow
9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{\sigma}e_{2}:\tau\dashv\Gamma^{\prime}$
then $\overset{\mathsf{val}}{\forall}_{\Gamma}.\left(\text{if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$ then
$e_{1}\cong e_{2}:\tau$}\right)$.

The above statements imply the soundness theorem. When
$\Gamma_{\textnormal{initial}}\vdash e_{1}\ext@arrow
9999{\arrowfill@\Leftarrow\Relbar\Rightarrow}{}{\sigma}e_{2}:\tau\dashv\Gamma^{\prime}$
we have
$\overset{\mathsf{val}}{\forall}_{\Gamma_{\textnormal{initial}}}.\left(\text{if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$ then
$e_{1}\cong e_{2}:\tau$}\right)$. Since $\Gamma_{\textnormal{initial}}$
contains only primitive operations, which are omitted from the
$\overset{\mathsf{val}}{\forall}_{\Gamma}.j$ judgment, the outer quantifier
quantifies over no variables, so we have that if
$\left(\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma\right)$ then
$e_{1}\cong e_{2}:\tau$. This together with the assumption that
$\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma$ allows us to
conclude that $e_{1}\cong e_{2}:\tau$. So for all expressions $e_{1}$ and
$e_{2}$, if $\Gamma_{\textnormal{initial}}\vdash e_{1}\ext@arrow
9999{\arrowfill@\Leftarrow\Relbar\Rightarrow}{}{\sigma}e_{2}:\tau\dashv\Gamma^{\prime}$
and $\overset{\mathsf{val}}{\forall}_{\Gamma^{\prime}}.\sigma$, then
$e_{1}\cong e_{2}:\tau$.

## Acknowledgments

This work was partially funded by National Science Foundation (Grants
CCF-1901381, CCF-1762363, and CCF-1629444).

## References

  * (1)
  * Ahmed et al. (2009) Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009.  State-dependent representation independence. In _Proc. Symposium on Principles of Programming Languages_. ACM, 340–353.  https://doi.org/10.1145/1480881.1480925
  * Ahmed (2006) Amal J. Ahmed. 2006\.  Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In _Proc. European Symposium on Programming_. Springer, 69–83.  https://doi.org/10.1007/11693024_6
  * Backes et al. (2013) John D. Backes, Suzette Person, Neha Rungta, and Oksana Tkachuk. 2013.  Regression Verification Using Impact Summaries. In _Proc. International Symposium Model Checking Software_. Springer, 99–116.  https://doi.org/10.1007/978-3-642-39176-7_7
  * Berman and Trevillyan (1989) C Leonard Berman and Louise H Trevillyan. 1989.  Functional comparison of logic designs for VLSI circuits. In _Proc. International Conference on Computer-Aided Design_. IEEE, 456–459.  https://doi.org/10.1109/ICCAD.1989.76990
  * Bobot et al. (2015) François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2015\.  Let’s verify this with Why3.  _Int. J. Softw. Tools Technol. Transf._ 17, 6 (2015), 709–727.  https://doi.org/10.1007/s10009-014-0314-5
  * Clarke et al. (2004) Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004\.  A tool for checking ANSI-C programs. In _Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems_. Springer, 168–176.  https://doi.org/10.1007/978-3-540-24730-2_15
  * Clarke et al. (2001) Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. 2001.  Bounded Model Checking Using Satisfiability Solving.  _Formal Methods Syst. Des._ 19, 1 (2001), 7–34.  https://doi.org/10.1023/A:1011276507260
  * de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems_. Springer, 337–340.  https://doi.org/10.1007/978-3-540-78800-3_24
  * Dreyer et al. (2009) Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2009.  Logical Step-Indexed Logical Relations. In _Proc. Annual Symposium on Logic in Computer Science_. IEEE Computer Society, 71–80.  https://doi.org/10.1109/LICS.2009.34
  * Fedyukovich et al. (2016) Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina. 2016\.  Property Directed Equivalence via Abstract Simulation. In _Proc. International Conference Computer-Aided Verification_. Springer, 433–453.  https://doi.org/10.1007/978-3-319-41540-6_24
  * Felsing et al. (2014) Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich. 2014\.  Automating regression verification. In _Proc. International Conference on Automated Software Engineering_. ACM, 349–360.  https://doi.org/10.1145/2642937.2642987
  * Godlin and Strichman (2009) Benny Godlin and Ofer Strichman. 2009.  Regression verification. In _Proc. Design Automation Conference_. ACM, 466–471.  https://doi.org/10.1145/1629911.1630034
  * Gulwani et al. (2018) Sumit Gulwani, Ivan Radicek, and Florian Zuleger. 2018\.  Automated clustering and program repair for introductory programming assignments. In _Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation_. ACM, 465–480.  https://doi.org/10.1145/3192366.3192387
  * Hur et al. (2012) Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012.  The marriage of bisimulations and Kripke logical relations. In _Proc. Symposium on Principles of Programming Languages_. ACM, 59–72.  https://doi.org/10.1145/2103656.2103666
  * Jaber (2020) Guilhem Jaber. 2020\.  SyTeCi: automating contextual equivalence for higher-order programs with references.  _PACMPL_ 4, POPL (2020), 59:1–59:28.  https://doi.org/10.1145/3371127
  * Kaleeswaran et al. (2016) Shalini Kaleeswaran, Anirudh Santhiar, Aditya Kanade, and Sumit Gulwani. 2016.  Semi-supervised verified feedback generation. In _Proc. International Symposium on Foundations of Software Engineering_. ACM, 739–750.  https://doi.org/10.1145/2950290.2950363
  * Koutavas and Wand (2006) Vasileios Koutavas and Mitchell Wand. 2006.  Small bisimulations for reasoning about higher-order imperative programs. In _Proc. Symposium on Principles of Programming Languages_. ACM, 141–152.  https://doi.org/10.1145/1111037.1111050
  * Liu et al. (2019) Xiao Liu, Shuai Wang, Pei Wang, and Dinghao Wu. 2019\.  Automatic grading of programming assignments: an approach based on formal semantics. In _Proc. International Conference on Software Engineering: Software Engineering Education and Training_. IEEE / ACM, 126–137.  https://doi.org/10.1109/ICSE-SEET.2019.00022
  * Perry et al. (2019) David Mitchel Perry, Dohyeong Kim, Roopsha Samanta, and Xiangyu Zhang. 2019.  SemCluster: clustering of imperative programming assignments based on quantitative semantic features. In _Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation_. 860–873.  https://doi.org/10.1145/3314221.3314629
  * Pu et al. (2016) Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay. 2016.  sk_p: a neural program corrector for MOOCs. In _Proc. International Conference on Systems, Programming, Languages and Applications: Software for Humanity_. ACM, 39–40.  https://doi.org/10.1145/2984043.2989222
  * Singh et al. (2013) Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama. 2013\.  Automated feedback generation for introductory programming assignments. In _Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation_. ACM, 15–26.  https://doi.org/10.1145/2491956.2462195
  * Sumii and Pierce (2005) Eijiro Sumii and Benjamin C. Pierce. 2005.  A bisimulation for type abstraction and recursion. In _Proc. Symposium on Principles of Programming Languages_. ACM, 63–74.  https://doi.org/10.1145/1040305.1040311
  * Wang et al. (2018) Ke Wang, Rishabh Singh, and Zhendong Su. 2018.  Search, align, and repair: data-driven feedback generation for introductory programming exercises. In _Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation_. ACM, 481–495.  https://doi.org/10.1145/3192366.3192384
  * Zuck et al. (2002) Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. 2002\.  VOC: A translation validator for optimizing compilers.  _Electronic notes in theoretical computer science_ 65, 2 (2002), 2–18.  https://doi.org/10.1016/S1571-0661(04)80393-1