We formalize Unlimited Register Machines and their operational semantics via (co)inductive types in Coq.
Our research has been published at INFINITY 2011, and the Coq script is available [here].
