16.9 Tail calls implementation

We assume the validity of machinery simplifications to focus on some aspect of the runtime behaviour, with the exception that we allow the compiler to perform tail calls optimisation (TCO), Simplification assumptions.