A coinductive semantics of the Unlimited Register Machine
Logic in Computer Science
2011-11-15 v1
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.
Cite
@article{arxiv.1111.3109,
title = {A coinductive semantics of the Unlimited Register Machine},
author = {Alberto Ciaffaglione},
journal= {arXiv preprint arXiv:1111.3109},
year = {2011}
}
Comments
In Proceedings INFINITY 2011, arXiv:1111.2678