基于大步长语义的迭代与递归统一推理
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
摘要：
可靠的演绎程序验证技术应该被证明是相对于程序设计语言的语义合理的。对于每一种不同的语言，构造一个单独的可靠性证明往往是一项艰巨的任务。在独立于语言的程序验证中，讨论了计算机程序的共同方面，以使所有语言都能进行合理的推理。在这项工作中，我们提出了一个解决方案，合理的推理迭代和递归的基础上的大步骤操作语义的任何程序设计语言。我们给出了我们的推理技术的合理性和相对完整性的归纳证明。我们说明了在简化的程序设计语言的命令式和功能的范例，具有不同的功能的技术。我们还在Coq证明助手中机制化所有正式结果。
英文摘要：
A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construction of a separate soundness proof is often a laborious undertaking. In language-independent program verification, common aspects of computer programs are addressed to enable sound reasoning for all languages. In this work, we propose a solution for the sound reasoning about iteration and recursion based on the big-step operational semantics of any programming language. We give inductive proofs on the soundness and relative completeness of our reasoning technique. We illustrate the technique at simplified programming languages of the imperative and functional paradigms, with diverse features. We also mechanism all formal results in the Coq proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
