% Version 0

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,proof,amsthm,amssymb,color,stmaryrd}
\usepackage{ifthen}
\usepackage{hyperref}
\newtheorem{theorem}{Theorem}
\usepackage{latexsym}
\usepackage{verbatim}
\usepackage{code,proof,amsthm,amssymb, amsmath}
\usepackage{ifthen}
\usepackage{graphics}
\usepackage{mathpartir}
\usepackage{float}
\usepackage{enumitem}
\usepackage{mathtools}
\usepackage{times}

% Macros that may be useful
% General stuff
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\irl}[1]{\mathtt{#1}}
\newcommand{\PFPL}{\emph{PFPL}}
\newcommand{\subst}[3]{[{#1}/{#2}]{#3}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PCF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% PCF stuff not related directly to types
\newcommand{\letbindabs}[3]{\irl{let}({#1};{#2}.{#3})}
\newcommand{\letbind}[3]{\irl{let}~{#2}={#1}~\irl{in}~{#3}}
\newcommand{\fixabs}[3]{\irl{fix}[{#1}]({#2}.{#3})}
\newcommand{\fix}[3]{\irl{fix}~{#2}{:}{#1}~\irl{is}~{#3}}

%% Natural numbers
\newcommand{\natt}{\irl{nat}}
\newcommand{\z}{\irl{z}}
\newcommand{\s}[1]{\irl{s}(#1)}
\newcommand{\ifzabs}[4]{\irl{ifz}({#1}; {#2}; {#3}.{#4})}
\newcommand{\ifz}[4]{\irl{ifz}~#1~\{\z \goesto #2~|~\s{#3}\goesto#4\}}

%% Functions
\newcommand{\parrtabs}[2]{\irl{parr}({#1}; {#2})}
\newcommand{\parrt}[2]{{#1} \rightharpoonup {#2}}
\newcommand{\lamabs}[3]{\irl{lam}[{#1}]({#2}.{#3})}
\newcommand{\lam}[3]{\irl{fn}\,({#2}{:}{#1})\,{#3}}
\newcommand{\apabs}[2]{\irl{ap}(#1; #2)}
\newcommand{\ap}[2]{#1~(#2)}

%% Products 
\newcommand{\unitt}{\irl{unit}}
\newcommand{\prodtabs}[2]{\irl{prod}({#1};{#2})}
\newcommand{\prodt}[2]{{#1}\times{#2}}
\newcommand{\trivabs}{\irl{triv}}
\newcommand{\triv}{\langle \rangle}
\newcommand{\pairabs}[2]{\irl{pair}({#1}; {#2})}
\newcommand{\pair}[2]{\langle {#1}, {#2} \rangle}
\newcommand{\prlabs}[1]{\irl{pr[l]}({#1})}
\newcommand{\prl}[1]{{#1}\cdot\irl{l}}
\newcommand{\prrabs}[1]{\irl{pr[r]}({#1})}
\newcommand{\prr}[1]{{#1}\cdot\irl{r}}

%% Sums
\newcommand{\voidt}{\irl{void}}
\newcommand{\sumtabs}[2]{\irl{sum}({#1}; {#2})}
\newcommand{\sumt}[2]{{#1} + {#2}}
\newcommand{\abort}[2]{\irl{abort}[#1](#2)}
\newcommand{\inltabs}[3]{\irl{in}[#1;#2][\irl{l}](#3)}
\newcommand{\inrtabs}[3]{\irl{in}[#1;#2][\irl{r}](#3)}
\newcommand{\inlt}[3]{\irl{inl}[#1;#2](#3)}
\newcommand{\inrt}[3]{\irl{inr}[#1;#2](#3)}
\newcommand{\ecase}[5]{\irl{case}~{#1}~\{\irl{inl}({#2}) \goesto {#3} \mid \irl{inr}({#4}) \goesto {#5}\}}
\newcommand{\ecaseabs}[5]{\irl{case}({#1};{#2}.{#3};{#4}.{#5})}

%% Recursive types
\newcommand{\recursivet}[2]{\mu{#1}.{#2}}
\newcommand{\recursivetabs}[2]{\irl{rec}({#1}.{#2})}
\newcommand{\fold}[3]{\irl{fold}[{#1}.{#2}]({#3})}
\newcommand{\unfold}[1]{\irl{unfold}({#1})}


\newcommand{\newabs}[2]{\irl{new}[{#1}]({#2})}
\newcommand{\new}[2]{{#1}\irl{!}\,{#2}}
\newcommand{\castabs}[4]{\irl{cast}[{#1}]({#2},{#3}.{#4})}
\newcommand{\cast}[4]{\irl{in{#1}}~{#3} = {#2}; {#4}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modernized Algol
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% judgments
\newcommand{\val}[1]{#1~\mathsf{val}}
\newcommand{\valS}[2]{#1~\mathsf{val}_{#2}}
\newcommand{\sctx}{\Sigma}
\newcommand{\valSC}[1]{\valS{#1}{\sctx}}
\newcommand{\stepsS}[3]{#1 \xmapsto[#2]{} #3}
\newcommand{\stepsSC}[2]{\stepsS{#1}{\sctx}{#2}}
\newcommand{\mobile}[1]{{#1}~\mathsf{mobile}}
\newcommand{\mem}{\mu}
\newcommand{\membinding}[2]{#1 \hookrightarrow #2}
\newcommand{\extmem}[3]{#1 \otimes (\membinding{#2}{#3})}
\newcommand{\emptymem}{\emptyset}
\newcommand{\state}[2]{#1 \parallel #2}
\newcommand{\final}[3]{\state{#1}{#2}~\mathsf{final}_{#3}}
\newcommand{\finalC}[2]{\final{#1}{#2}{\sctx}}
\newcommand{\err}[3]{\state{#1}{#2}~\mathsf{err}_{#3}}
\newcommand{\errC}[2]{\err{#1}{#2}{\sctx}}

\newcommand{\dom}[1]{\text{dom}(#1)}

% types
\newcommand{\nat}{\mathtt{nat}}
\newcommand{\cmd}[1]{\mathtt{cmd}(#1)}

% assignables
\newcommand{\cmdget}{\mathtt{get}}
\newcommand{\cmdset}{\mathtt{set}}
\newcommand{\erefabs}[1]{\irl{ref}[{#1}]}
\newcommand{\eref}[1]{\texttt{\&}{#1}}

\newcommand{\cmdret}{\mathtt{ret}}
\newcommand{\ret}[1]{\mathtt{ret}~#1}
\newcommand{\retabs}[1]{\mathtt{ret}(#1)}
\newcommand{\bnd}[3]{\mathtt{bnd}~{#2} \leftarrow {#1}; {#3}}
\newcommand{\bndabs}[3]{\mathtt{bnd}({#1}; {#2}.{#3})}
\newcommand{\dcl}[3]{\mathtt{dcl}~{#2} := {#1}~\mathtt{in}~{#3}}
\newcommand{\dclabs}[3]{\mathtt{dcl}[\tau]({#1}; {#2}.{#3})}
\newcommand{\mget}[1]{\mathtt{@}#1}
\newcommand{\getabs}[1]{\mathtt{get}[#1]}
\newcommand{\mset}[2]{#1 := #2}
\newcommand{\setabs}[2]{\mathtt{set}[{#1}]({#2})}
\newcommand{\getrefabs}[1]{\mathtt{getref}({#1})}
\newcommand{\setrefabs}[2]{\mathtt{setref}({#1}; {#2})}
\newcommand{\getref}[1]{\texttt{*}{#1}}
\newcommand{\setref}[2]{{#1} := {#2}}
%\newcommand{\dummy}{\underline{\hspace{0.5em}}}


% surface syntax
\newcommand{\seqabs}[3]{\irl{seq}(#2; #1.#3)}
\newcommand{\seq}[3]{\{#1 \leftarrow #2; #3\}}
\newcommand{\doabs}[1]{\irl{do}(#1)}
\newcommand{\mdo}[1]{\irl{do}(#1)}
\newcommand{\ifabs}[3]{\irl{if}(#1; #2; #3)}
\newcommand{\mif}[3]{\irl{if}~(#1)~#2~\irl{else}~#3}
\newcommand{\whileabs}[2]{\irl{while}({#1};{#2})}
\newcommand{\mwhile}[2]{\irl{while}({#1})~{#2}}
\newcommand{\callabs}[2]{\irl{call}({#1}; {#2})}
\newcommand{\mcall}[2]{{#1}\,({#2})}

% - nat
\newcommand{\suc}{\mathtt{s}}
\renewcommand{\bar}[1]{\overline{#1}}

% - products
% ex: \langle \m{a}\hooksto\unit, \m{b}\hooksto\nat \rangle$.
\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\proj}{\cdot}
\newcommand{\pr}{\cdot}

% misc syntax
\newcommand{\letmabs}[3]{\irl{letm}({#1};{#2}.{#3})}
\newcommand{\letm}[3]{\irl{letm} ~{#2} = {#1} ~ \irl{in} ~ #3}
\newcommand{\exprlet}{\mathsf{let}}
\newcommand{\letexpr}{\mathsf{let}}
\newcommand{\elet}{\mathsf{let}}
\newcommand{\lete}{\mathsf{let}}
\newcommand{\letproc}{\irl{letproc}}
\newcommand{\procabs}[5]{\irl{proc}[{#1};{#2}]({#3}.{#4}.{#5})}
\newcommand{\proc}[5]{\irl{proc} ~{#3}~ {({#4} : {#1})} : {#2} = {#5}}
\newcommand{\cmddo}{\mathsf{do}}

% procedures
\newcommand{\procedure}[5]{\irl{procedure}~#1~(#2:#3)~\irl{is}~#4~\irl{in}~#5}
\newcommand{\procown}[7]{\irl{procedure}~#1~(#2:#3)~\irl{own}~#4:=#5~\irl{is}~#6~\irl{in}~#7}

% object macro
\newcommand{\method}[4]{\irl{method}~\irl{#1}(#2:#3)~\irl{is}~{#4}}
\newcommand{\obj}[6]{\irl{object}~#1~\irl{is}~\irl{field}~#2:=#3~\irl{with}~#4~\irl{and}~#5~\irl{in}~#6}


\newcommand{\qbox}{\fbox{???}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% System F
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% definition
\newcommand{\defeq}{\triangleq}

% types
\newcommand{\ordt}{\mathtt{ord}}
\newcommand{\poly}[2]{\forall #1.#2}
\newcommand{\existt}[2]{\exists #1.#2}

\newcommand{\cmdt}[1]{\mathtt{cmd}(#1)}
\newcommand{\reft}[1]{\mathtt{ref}(#1)}
\newcommand{\sumabs}[2]{\mathtt{sum}(#1; #2)}
\newcommand{\rect}[2]{\irl{rec}(#1.#2)}


% expressions 
\newcommand{\case}{\mathtt{case}}
\newcommand{\rec}{\mathtt{rec}}

% - nat
% \zero
% \succ
\newcommand{\iternat}[4]{\iter_\natt(#1;#2;#3.#4)}

% - ord (constructors)
\newcommand{\LT}{\mathtt{LT}}
\newcommand{\EQ}{\mathtt{EQ}}
\newcommand{\GT}{\mathtt{GT}}
\newcommand{\caseord}[4]{\case_\ordt(#1;#2;#3;#4)}
% \case_\ordering

% - list (constructors)
\newcommand{\nil}{\mathtt{nil}}
\newcommand{\cons}[2]{\mathtt{cons}(#1;#2)}
\newcommand{\iterlist}[5]{\iter_\listt(#1;#2;#3.#4.#5)}

% - trees (constructors)
\newcommand{\exprempty}{\mathtt{empty}} 
\newcommand{\emptytree}{\mathtt{empty}} 
\newcommand{\treeempty}{\mathtt{empty}} 
\newcommand{\eempty}{\mathtt{empty}} 
\newcommand{\branch}[3]{\mathtt{branch}(#1;#2;#3)}
\newcommand{\exprbranch}{\branch}
\newcommand{\branchtree}{\branch}
\newcommand{\treebranch}{\branch}
\newcommand{\ebranch}{\branch}
\newcommand{\itertree}[6]{\iter_\treet(#1;#2;#3.#4.#5.#6)}

% - products
\newcommand{\projl}{\cdot\mathsf{l}}
\newcommand{\projr}{\cdot\mathsf{r}}

% - sums

\newcommand{\ldyn}{\mathcal{L}\{\textit{dyn}\}}
\newcommand{\lhpcf}{\mathcal{L}(\mathtt{nat} \rightharpoonup \dynt)}
\newcommand{\lstat}{\mathcal{L}(\mathtt{nat} \rightharpoonup \mu +)}

% - polymorphism
\newcommand{\Lam}[2]{\Lambda #1.#2}
\newcommand{\tap}[2]{#1[#2\]}
\newcommand{\Tap}{\tap}

% - existential
\newcommand{\pack}[4]{\irl{pack}~#1~\irl{with}~#2~\irl{as}~\existt{#3}{#4}}
\newcommand{\open}[5]{\irl{open}~#1~\irl{as}~#2~\irl{with}~\hasType{#3}{#4}~\irl{in}~#5}


\newcommand{\num}[1]{\irl{num}[#1]}
\newcommand{\numeral}[1]{\bar{#1}}
\newcommand{\zero}{\irl{zero}}
\renewcommand{\succ}[1]{\irl{succ}(#1)}

\newcommand{\ok}{\irl{ok}}
\newcommand{\isnum}[2]{#1~\textsf{is\_num}~#2}
\newcommand{\isntnum}[1]{#1~\textsf{isnt\_num}}
\newcommand{\isfun}[3]{#1~\textsf{is\_fun}~#2.#3}
\newcommand{\isntfun}[1]{#1~\textsf{isnt\_fun}}

\newcommand{\numc}{\irl{num}}
\newcommand{\func}{\irl{fun}}


\newcommand{\letexp}[3]{\irl{let}(#2; \abst{#1}{#3})}
\newcommand{\parrabs}[2]{\irl{parr}(#1; #2)}
\newcommand{\parr}[2]{#1 \rightharpoonup #2}
\newcommand{\arr}[2]{#1 \rightarrow #2}


%\newcommand{\ok}[1]{#1~\sf{ok}}



\newcommand{\dynd}{\dynt^\dagger}

\newcommand{\error}[1]{\irl{error}[#1]}


\newcommand{\intro}{\text{-I}}
\newcommand{\elim}{\text{-E}}

\newcommand{\abst}[2]{#1.#2}
\newcommand{\steps}[2]{#1 \mapsto #2}

\newcommand{\goesto}{\Rightarrow}

\newcommand{\translates}{\Longrightarrow}
\newcommand{\trans}[2]{#1 \translates #2}

\newcommand{\proves}{\vdash}
\newcommand{\hasType}[2]{#1 : #2}
\newcommand{\hasTypem}[2]{#1 \sim #2}
\newcommand{\bindType}[2]{#1{:}#2}
\newcommand{\typeJ}[3]{#1 \proves \hasType{#2}{#3}}
\newcommand{\ctx}{\Gamma}
\newcommand{\emptyCtx}{\emptyset}
\newcommand{\xCtx}[2]{\ctx, \hasType{#1}{#2}}
\newcommand{\typeJC}[2]{\typeJ{\ctx}{#1}{#2}}
\newcommand{\typeJF}[4]{\typeJ{\ctxf{#1}{#2}}{#3}{#4}}
\newcommand{\typeJCF}[2]{\typeJ{\ctxf{\tctx}{\ctx}}{#1}{#2}}

\newcommand{\typeJA}[4]{{#1} \proves_{#2} \hasType{#3}{#4}}
\newcommand{\typeJAm}[4]{{#1} \proves_{#2} \hasTypem{#3}{#4}}
\newcommand{\typeJCA}[2]{\typeJA{\ctx}{\sctx}{#1}{#2}}
\newcommand{\typeJCAm}[2]{\typeJAm{\ctx}{\sctx}{#1}{#2}}

\newcommand{\type}[1]{#1~\mathsf{type}}
\newcommand{\tctx}{\Delta}
\newcommand{\tformJ}[2]{#1 \vdash \type{#2}}
\newcommand{\tformJC}[1]{\tformJ{\tctx}{#1}}

\newcommand{\ctxf}[2]{#1~#2}
\newcommand{\ctxfDef}{\ctxf{\tctx}{\ctx}}

\newcommand{\tlrule}{\theta\Lambda}
\newcommand{\valrule}{\textsf{v}}
\newcommand{\progrule}{\textsf{s}}
\newcommand{\elimrule}{\textsf{e}}
\newcommand{\typerule}{\textsf{t}}

\newcommand{\laz}[1]{\left[ #1 \right]}


\title{Assignment 4:
       Imperative Programming with Algol}
\author{15-312: Principles of Programming Languages}
\date{Name: CHANGE ME $\rightarrow$ Harry Bovik (hbovik) $\leftarrow$ CHANGE ME\\
Recitation: B}


\begin{document}
\noindent
\maketitle

\paragraph{Task 1.1 (Preservation, 15\%)}

\begin{itemize}
\item $\mathcal{P}(\stepsSC{\state{m}{\mem}}{\state{m'}{\mem'}})$ is ``\ldots''
\end{itemize}

\begin{itemize}
\item Case for rule (17) $\inferrule{ }{
	\stepsS{
		\state{\getabs{a}}{\extmem{\mem}{a}{e}}
	}{\sctx, \hasTypem{a}{\tau}}{
		\state{\retabs{e}}{\extmem{\mem}{a}{e}}
	}}$
\begin{tabbing}
\textit{To show} \ldots
\end{tabbing}

\item Case for rule (20): $\inferrule{
	\stepsSC{e}{e'}
}{
	\stepsSC{
		\state{\dclabs{e}{a}{m}}{\mem}
	}{
		\state{\dclabs{e'}{a}{m}}{\mem}
	}
}$
\begin{tabbing}
\textit{To show} \ldots
\end{tabbing}

\item Case for rule (21): $\inferrule{
	\valSC{e}\\
	\stepsS{
		\state{m}{\extmem{\mu}{a}{e}}
	}{\sctx, \hasTypem{a}{\tau}}{
		\state{m'}{\extmem{\mu'}{a}{e'}}
	}
}{
	\stepsSC{
		\state{\dclabs{e}{a}{m}}{\mem}
	}{
		\state{\dclabs{e'}{a}{m'}}{\mem'}
	}
}$
\begin{tabbing}
\textit{To show} \ldots
\end{tabbing}

\item Case for rule (22): $\inferrule{
	\valSC{e}\\
	\valS{e'}{\sctx, \hasTypem{a}{\tau}}
}{
	\stepsSC{
		\state{\dclabs{e}{a}{\retabs{e'}}}{\mem}
	}{
		\state{\retabs{e'}}{\mem}
	}
}$
\begin{tabbing}
\textit{To show} \ldots
\end{tabbing}
\end{itemize}

\noindent
Additional inversion lemmas used (do not prove):
\begin{itemize}
\item \ldots
\end{itemize}

\paragraph{Task 1.2 (Progress, 15\%)}

\begin{itemize}
\item $\mathcal{P}(\typeJA{\Gamma}{\sctx}{e}{\tau})$ is ``\ldots''
\item $\mathcal{P}(\typeJAm{\Gamma}{\sctx}{m}{\tau})$ is ``\ldots''
\end{itemize}

\noindent
Additional canonical forms lemmas used (do not prove):
\begin{itemize}
\item \ldots
\end{itemize}


\paragraph{Task 1.3 (Counterexample, 5\%)}

The rules are repeated here, in part to illustrate the judgments used
in this assignment. Please remove both the rules below and the 
figure on the next page from your handin.

\begin{mathpar}
\small
\inferrule
{\typeJCA{e}{\sumt{\tau_1}{\tau_2}}}
{\typeJCAm{e\,@\,\irl{l}}{\tau_1}}

\inferrule
{\typeJCA{e}{\sumt{\tau_1}{\tau_2}}}
{\typeJCAm{e\,@\,\irl{r}}{\tau_2}}\\

\inferrule
{\stepsSC{e}{e'}}
{\stepsSC{\state{e\,@\,\irl{l}}{\mem}}{\state{e'\,@\,\irl{l}}{\mem}}}

\inferrule
{\valSC{\inltabs{\tau_1}{\tau_2}{e}}}
{\stepsSC{\state{\inltabs{\tau_1}{\tau_2}{e}\,@\,\irl{l}}{\mem}}
         {\state{\ret{e}}{\mu}}}

\inferrule
{\valSC{\inrtabs{\tau_1}{\tau_2}{e}}}
{\errC{\inrtabs{\tau_1}{\tau_2}{e}\,@\,\irl{l}}{\mem}}\\

\inferrule
{\stepsSC{e}{e'}}
{\stepsSC{\state{e\,@\,\irl{r}}{\mem}}{\state{e'\,@\,\irl{r}}{\mem}}}

\inferrule
{\valSC{\inrtabs{\tau_1}{\tau_2}{e}}}
{\stepsSC{\state{\inrtabs{\tau_1}{\tau_2}{e}\,@\,\irl{r}}{\mem}}
         {\state{\ret{e}}{\mu}}}

\inferrule
{\valSC{\inltabs{\tau_1}{\tau_2}{e}}}
{\errC{\inltabs{\tau_1}{\tau_2}{e}\,@\,\irl{r}}{\mem}}\\
\end{mathpar}


\begin{figure}
\[
\begin{array}{l c c l l}
\textbf{Sort} & & & \textbf{Abstract Form} & \textbf{Concrete Form}\\
\ms{Type} & \tau  & ::= & \natt                     & \natt\\
          &       &     & \parrtabs{\tau_1}{\tau_2} & \parrt{\tau_1}{\tau_2}\\
          &       &     & \unitt                    & \unitt\\
          &       &     & \prodtabs{\tau_1}{\tau_2} & \prodt{\tau_1}{\tau_2}\\
          &       &     & \voidt                    & \voidt\\
          &       &     & \sumtabs{\tau_1}{\tau_2}  & \sumt{\tau_1}{\tau_2}\\
          &       &     & \recursivetabs{t}{\tau}   & \recursivet{t}{\tau}\\
          &       &     & \cmdt{\tau}               & \cmdt{\tau} \\
          &       &     & \reft{\tau}               & \reft{\tau} \\
\ms{Exp}  & e & ::= & x                         & x\\
          &   &     & \z                        & \z\\
          &   &     & \s{e}                     & \s{e}\\
          &   &     & \ifzabs{e}{e_0}{x}{e_1}   & \ifz{e}{e_0}{x}{e_1}\\
          &   &     & \letbindabs{e_0}{x}{e_1}   
                                         & \letbind{e_0}{x}{e_1}\\
          &   &     & \lamabs{\tau}{x}{e}       & \lam{\tau}{x}{e}\\
          &   &     & \apabs{e_1}{e_2}          & \ap{e_1}{e_2}\\
          &   &     & \fixabs{\tau}{x}{e}       & \fix{\tau}{x}{e}\\
          &   &     & \abort{\tau}{e}           & \abort{\tau}{e}\\
          &   &     & \inltabs{\tau_1}{\tau_2}{e} 
                                         & \inlt{\tau_1}{\tau_2}{e} \\
          &   &     & \inrtabs{\tau_1}{\tau_2}{e}  
                                         & \inrt{\tau_1}{\tau_2}{e} \\
          &   &     & \ecaseabs{e}{x_1}{e_1}{x_2}{e_2}
                                         & \ecase{e}{x_1}{e_1}{x_2}{e_2} \\
          &   &     & \trivabs                  & \triv\\
          &   &     & \pairabs{e_1}{e_2}        & \pair{e_1}{e_2}\\
          &   &     & \prlabs{e}                & \prl{e}\\
          &   &     & \prrabs{e}                & \prr{e}\\
          &   &     & \fold{t}{\tau}{e}         & \fold{t}{\tau}{e}\\
          &   &     & \unfold{e}                & \unfold{e}\\
          &   &     & \cmd{m}                   & \cmd{m}\\
          &   &     & \erefabs{a}               & \eref{a}\\
\ms{Cmd}  & m & ::= &  \retabs{e}               & \ret{e}\\
          &   &     & \bndabs{e}{x}{m}          & \bnd{e}{x}{m}\\
          &   &     & \dclabs{e}{a}{m}          & \dcl{e}{a}{m}\\
          &   &     & \getabs{a}                & \mget{a}\\
          &   &     & \setabs{a}{e}             & \mset{a}{e}\\
          &   &     & \getrefabs{e}             & \getref{e}\\
          &   &     & \setrefabs{e_1}{e_2}      & \setref{e_1}{e_2}\\
          &   &     & \castabs{l}{e}{x}{m}      & \cast{l}{e}{x}{m}\\
          &   &     & \castabs{r}{e}{x}{m}      & \cast{r}{e}{x}{m}\\
\end{array}
\]
\caption{Expressions and types in our version of Modernized Algol}
\end{figure}

\end{document}
