A coinductive semantics of the Unlimited Register Machine
arXiv:1111.3109 · doi:10.4204/EPTCS.73.7
Abstract
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type theory. Our formalization allows us to certify the implementation of partial functions, thus it can be regarded as a first step towards the development of a workbench for the formal analysis and verification of both converging and diverging computations.
In Proceedings INFINITY 2011, arXiv:1111.2678