\begin{figure}
Compatibility between values, outcomes and return types:

$$\begin{array}{rclr}
"Out_normal", "Tvoid" & \#  & "Vundef"&  \\
"Out_normal", "Tvoid" & \#  & "Vundef"&  \\
"Out_return", \, "Tvoid" & \# & "Vundef" & \\
"Out_return" \some v, \, \tau & \# & v & \mbox{when}\,\tau~\not="Tvoid"
\end{array}$$

\numberrules

Function calls:
\begin{pannel}

\irule
        G, E |- {a_{fun}}^{\tau}, M \evalexpr v_{fun}, \tr_1, M_1 &
        G, E |- a_{args}, M_1 \evalexpr v_{args}, \tr_2, M_2 \\
        G[v_{fun}] = \some{f} &
        "type_of_fundef" (f) = \tau  \\
        G |- f(v_{args}), M_2 \evalfunc v_{res}, \tr_3, M_3
        --------------------------------------------------
        G, E |-  {({a_{fun}}^{\tau}  (a_{args}))}^{\tau'}, M \evalexpr v_{res}, \cat {\cat {\tr_1} \tr_2} \tr_3, M_3
\end \label{rule:25}
\end{pannel}

Function invocations:
\begin{pannel}

\irule
        "alloc" ({\it \emptyset_E}, M, "params" (f) + "vars" (f),E) = (M_1, b) \\
        "bind_params" (E, M_1, "params" (f), v_{args}) = M_2 \\
        G, E |- "body" (f), M_2 \evalstmt \out, \tr, M_3 \\
        \out, \, "fn_return" (f) \, "#" \, v_{res}
        --------------------------------------------------
        G, E |- f(v_{args}), M \evalstmt v_{res}, \tr, "free" (M_3, b)
\end \label{rule:26}

\irule
        v_{args}, v_{res}  \cong^{\sigma} e_{args}, e_{res} 
        --------------------------------------------------
        G, E |- <\id \, \sigma>(v_{args}), M \evalstmt v_{res}, [\id \,e_{args}\, e_{res}], M
\end \label{rule:27}

\end{pannel}
\caption{Dynamic semantics of function call}
\label{fig:dynsem3}
\end{figure}