LARA

Type Rules for Block Statement

Note that variable declarations are allowed in blocks

  • we type statements one by one
  • declarations introduce new bindings into the environment

We apply these rules (with those listed first having higher priority):

\begin{equation*}
\Gamma \vdash \{\} : void
\end{equation*}

\begin{equation*}
\frac{\Gamma \vdash e : T}
     {\Gamma \vdash \{\textbf{return}\ e\} : T}
\end{equation*}

\begin{equation*}
\frac{\Gamma \oplus \{x \mapsto T_1\} \vdash \{ s_2 \ldots\ s_n\} : T}
     {\Gamma \vdash \{ T_1\, x; s_2\ \ldots\ s_n \} : T}
\end{equation*}

\begin{equation*}
\frac{\Gamma \vdash s_1 : void,\ \Gamma \vdash \{ s_2 \ldots\ s_n\} : T}
     {\Gamma \vdash \{ s_1\ s_2\ \ldots\ s_n \} : T}
\end{equation*}