A coinductive semantics of the Unlimited Register Machine

Details A coinductive semantics of the Unlimited Register Machine A coinductive semantics of the Unlimited Register Machine

2011-11-14

arxiv.org/abs/1111.3109v1

EPTCS 73, 2011, pp. 49-63

Computer Science

Logic in Computer Science

In Proceedings INFINITY 2011, arXiv:1111.2678

Scientific paper

10.4204/EPTCS.73.7

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.

Affiliated with

Also associated with

No associations

Rating

A coinductive semantics of the Unlimited Register Machine does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A coinductive semantics of the Unlimited Register Machine, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A coinductive semantics of the Unlimited Register Machine will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-216685