A coinductive semantics of the Unlimited Register Machine
Alberto Ciaffaglione (University of Udine)
TL;DR
This paper presents a formal coinductive semantics for the Unlimited Register Machine within Coq, enabling certification of partial functions and paving the way for rigorous analysis of converging and diverging computations.
Contribution
It introduces a coinductive approach to formalize URM evaluation in Coq, allowing for verification of partial functions and divergence.
Findings
Formalization of URM evaluation in Coq
Certification of partial functions
Foundation for analyzing diverging computations
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Security and Verification in Computing