\begin{figure}[p]
    \begin{leftfullpage}
        \begin{footnotesize}
            \noindent Statement: \hfill\framebox{$\Phi;\Gamma \vdash \HL{s} : t$}
            \begin{mathpar}
                \inferrule*[left=TS-Skip]
                {
                }
                {
                    \Phi;\Gamma |- \HL{\codebf{skip}} : \bot
                }
                \and
                \inferrule*[left=TS-Ret]
                {
                    \Phi;\Gamma |- \HL{e} : t
                }
                {
                    \Phi;\Gamma |- \HL{\codebf{return}\ e;} : t
                }
                \and
                \inferrule*[left=TS-Expr]
                {
                    \Phi;\Gamma |- \HL{e} : t \\
                    \Phi;\Gamma |- \HL{s} : t_r
                }
                {
                    \Phi;\Gamma |- \HL{e;\ s} : t_r
                }
                \and
                \inferrule*[left=TS-Decl]
                {
                    \Phi;\Gamma[x \mapsto t] |- \HL{s} : t_r
                }
                {
                    \Phi;\Gamma |- \HL{t\ x;\ s} : t_r
                }
                \and
                \inferrule*[left=TS-Assign]
                {
                    x : t \in \Gamma \\
                    \Phi;\Gamma |- \HL{e} : t \\
                    \Phi;\Gamma |- \HL{s} : t_r
                }
                {
                    \Phi;\Gamma |- \HL{x = e;\ s} : t_r
                }
                \and
                \inferrule*[left=TS-If]
                {
                    \Phi;\Gamma |- \HL{e} : \codebf{bool} \\
                    \Phi;\Gamma |- \HL{s_t} : \bot \\
                    \Phi;\Gamma |- \HL{s_f} : \bot \\
                    \Phi;\Gamma |- \HL{s_r} : t_r
                }
                {
                    \Phi;\Gamma |- \HL{\codebf{if}\ (e)\ s_t\ \codebf{else}\ s_f\ s_r} : t_r
                }
                \and
                \inferrule*[left=TS-While]
                {
                    \Phi;\Gamma |- \HL{e} : \codebf{bool} \\
                    \Phi;\Gamma |- \HL{s_b} : \bot \\
                    \Phi;\Gamma |- s_r : t_r
                }
                {
                    \Phi;\Gamma |- \HL{\codebf{while}\ (e)\ s_b\ s_r} : t_r
                }
            \end{mathpar}
            \hrule
            \smallskip
            \noindent Expression: \hfill\framebox{$\Phi;\Gamma \vdash \HL{e} : t$}
            \begin{mathpar}
                \inferrule*[left=TE-Var]
                {
                    x : t \in \Gamma
                }
                {
                    \Phi;\Gamma |- \HL{x} : t
                }
                \and
                \inferrule*[left=TE-Val]
                {
                }
                {
                    \Phi;\Gamma |- \HL{\val_t} : t
                }
                \and
                \inferrule*[left=TE-Call]
                {
                    \HL{t_r\ \ell(t_1\ x_1,\ldots,t_n\ x_n)\ \{\ s\ \}} \in \Phi \\
                    \Phi;\Gamma |- \HL{e_1} : t_1 \\
                    \cdots \\
                    \Phi;\Gamma |- \HL{e_n} : t_n
                }
                {
                    \Phi;\Gamma |- \HL{\ell(e_1,\ldots,e_n)} : t_r
                }
                \and
                \inferrule*[left=TE-Stmt]
                {
                    \Phi;\Gamma |- \HL{s} : t
                }
                {
                    \Phi;\Gamma |- \HL{\stmtexpr{s}{\sigma}} : t
                }
            \end{mathpar}
        \end{footnotesize}%
        \caption{Typing in \imp}
        \label{sierra:fig:rules_t_imp}
    \end{leftfullpage}
\end{figure}