Lecture 19: Compilation: The CPM machine

With this lecture we leave the formal world of the meta level of Twelf and return to applications. The application which is in the center of this lecture is the CPM machine. We motivate how the machine works, develop its operational semantics, and we prove the completeness direction of its equivalence to the big step operational semantics for Mini-ML introduced in Lecture 2