$4$ Sums

Task $4\mathrm{.}1(15$ points$).$

Add sums $($and their intro and elim forms$)$ to our treatment of evaluation contexts:

$1.$ Define the additional syntactic forms for evaluation contexts $E$ for contexts involving inl, inr and case.

$2.$ Define the additional rules for the judgment $E$:${}^{\text{'}}.$ You should have one new rule for each new evaluation context you defined above.

$3.$ Prove the additional cases for Lemma $1$ from class, for the rules you defined above.

Recall Lemma $1$: If $E$:${}^{\text{'}}$ and $*|-e$:$$ then $*|-E[e]$:${}^{\text{'}}.$

Task $4\mathrm{.}2(15$ points$).$

Add sums $($and their intro and elim forms$)$ to our treatment of control stacks:

$1.$ Define the additional syntactic forms for stack frames $f$ involving inl, inr and case.

$2.$ Define the additional step rules $($e$.$g$.,$ S$-1)$ for inl, inr and case. Use the rules we defined so far as a guide. You need rules that start with states of the form $ke$ as well as some that start with states

of the form $kv.$

$3.$ Define the additional typing rules $($e$.$g$.,$ F$-1)$ for the stack frames you defined in part $1.$

Note: no need to prove anything