机械化语义
摘要：使用现代定理证明器（在本案例中为Coq证明助手），展示如何对编程语言及其语义进行机械化规范，并对个体程序和通用程序转换进行推理，如编译器中常见的情况。讨论的主题包括：操作语义（小步、大步、定义性解释器）；简单形式的指示性语义；公理性语义和Hoare逻辑；生成验证条件，并应用于程序证明；编译成虚拟机代码及其正确性证明；一个优化程序转换（死代码消除）的示例及其正确性证明。
作者：Xavier Leroy (INRIA Rocquencourt)
论文ID：1010.5582
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-10-28