A coinductive semantics of the Unlimited Register Machine

Alberto Ciaffaglione
(University of Udine)

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 Fang Yu and Chao Wang: Proceedings 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011), Taipei, Taiwan, 10th October 2011, Electronic Proceedings in Theoretical Computer Science 73, pp. 49–63.
Published: 11th November 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.73.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org