Let f \mapsto \tau\ f(\tau_1\,x_1, \ldots, \tau_k\,x_k)\ \{c\} be in the program. The environment of the function holds only the parameters, because there are no global variables.

Each argument is checked at the type of its parameter by the judgment \Gamma \vdash e \lhd \tau of Definition 5.3.1, so that a lambda may be an argument. A variable f of function type in \Gamma hides the function named f, and the call is then Definition 5.3.3.

\dfrac{f \notin \Gamma \qquad \Gamma \vdash e_i \lhd \tau_i \quad (1 \le i \le k)}{\Gamma \vdash f(e_1, \ldots, e_k) : \tau}\;\textsf{(T-Call)}

\dfrac{\begin{array}{c} \rho, \sigma_{i-1} \vdash e_i \Rightarrow v_i, \sigma_i \quad (1 \le i \le k,\ \sigma_0 = \sigma) \\ (\ell_i, \sigma'_i) = \mathrm{alloc}(\sigma'_{i-1}, v_i) \quad (1 \le i \le k,\ \sigma'_0 = \sigma_k) \\ [x_1 \mapsto \ell_1, \ldots, x_k \mapsto \ell_k], \sigma'_k \vdash c \Rightarrow \mathsf{ret}\,v, \rho', \sigma'' \end{array}}{\rho, \sigma \vdash f(e_1, \ldots, e_k) \Rightarrow v, \sigma'' \setminus (\{\ell_1, \ldots, \ell_k\} \cup (\rho' \setminus \rho_f))}\;\textsf{(Call)}

The return frees the copies of the arguments and the locals the body declared, \rho' \setminus \rho_f read as the owned bindings the body added, so after a call the store holds only what existed before it and the objects created with new.

When the body ends with \mathsf{normal}, the result is \mathsf{void} if \tau = \mathsf{void} and error otherwise. A missing return in a non void function is an evaluation error, not a type error.

The rule above is the case in which every parameter is by value, and Definition 5.2.1 gives the case of a parameter by reference.

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.