The \C{Compute} command is not exactly the \c{compute} tactic, right? Better to say either \C{Compute} or \C{vm_compute}.
"Expected value" sounds too much like the probability-theoretic concept of the same name. I suggest "explicit result" instead.
Functions with several arguments are "not represented" -> "not usually represented" with a tuple of arguments, since you can (if you really want) use Cartesian product types.
I'm not sure what "it appends that" means in French, but it's not idiomatic in English.
Added \hypersetup to main.tex so that the title and author metadata in the resulting PDF are meaningful.
The \C{Compute} command is not exactly the \c{compute} tactic, right? Better to say either \C{Compute} or \C{vm_compute}.
"Expected value" sounds too much like the probability-theoretic concept of the same name. I suggest "explicit result" instead.
Functions with several arguments are "not represented" -> "not usually represented" with a tuple of arguments, since you can (if you really want) use Cartesian product types.
I'm not sure what "it appends that" means in French, but it's not idiomatic in English.
Added \hypersetup to main.tex so that the title and author metadata in the resulting PDF are meaningful.