Paper Info
Title
A Coinductive Semantics Of The Unlimited Register Machine
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.
Year
DOI
Venue
2011
10.4204/EPTCS.73.7
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Volume
Workbench,Programming language,Computer science,Type theory,Theoretical computer science,Mathematical proof,Coinduction,Register machine,Semantics,Partial function,Proof assistant
Journal
73
Issue
ISSN
Citations 
73
2075-2180
2
PageRank 
References 
Authors
0.43
11
1
Name
Order
Citations
PageRank
Alberto Ciaffaglione1589.97