First draft of BVL (bytecode-value language).

The semantics is defined as an evaluation function.

This commit includes the correctness proof of a
simple optimisation: inlining of a function body.