A function is well typed when its parameter and return types have values
and are well formed, and its body is, under the context of its parameters and
its return type. A reference parameter has in Γ the type of its referent, as a
local reference does.

```
τ, τᵢ storable and well formed    [x₁ ↦ τ₁, …, xₖ ↦ τₖ] ⊢ c ⊣ Γ'
──────────────────────────────────────────────────────────────── (T-Fun)
⊢ τ f (τ₁ x₁, …, τₖ xₖ) { c }
```

A program is well typed when class and function names are distinct up to
overloading, every class and function is well typed and `int main()` exists.
A template is not checked, only its instantiations are.

```
names distinct up to overloading    ⊢ Cᵢ for each class    ⊢ fᵢ for each function
main ↦ (int main() { c })
────────────────────────────────────────────────────────────────────────────── (T-Program)
⊢ p
```

Program execution. The initial store is empty, because there are no global
variables, and the result is the value returned by `main()`.

```
main ↦ (int main() { c })    [], ∅ ⊢ main() ⇒ v, σ
─────────────────────────────────────────────────── (Program)
p ⇒ v
```

The objects created with new stay in σ until delete or the end of the
program. The locals of main leave σ with the return of the call, so the
final store holds objects only. The program is annotated with the static
classes of method calls and deletes before it runs, when it is well typed,
and otherwise runs as parsed, with every dispatch by the class tag.