无限寄存器机的共归纳语义
A coinductive semantics of the Unlimited Register Machine
摘要：
我们利用（共）归纳规范和证明的方法来评估低层次的程序无限注册机（URM）的Coq系统，一个证明助手的基础上演算（共）归纳结构类型论。我们的形式化使我们能够证明部分功能的实现，因此，它可以被看作是第一步的工作台的正式分析和验证收敛和发散计算的发展。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
