Complete and formalize all the definitions and operational semantics in the paper. The goal would be to be able to run semantics and the CPS translation.