共归大步操作语义
摘要：使用一种按值调用的函数式语言作为例子，本文演示了在大步操作语义中使用共归纳定义和证明的方法，使其能够描述终止和发散的评估。我们将共归纳的大步语义与标准的小步语义之间的联系进行了形式化，并证明了这两种语义是等价的。然后我们研究了使用共归纳的大步语义在类型完备性证明和编译器语义保持性证明中的应用。本文的方法学特点是所有的结果都使用Coq证明助手进行了证明。我们解释了Coq提供的共归纳定义和证明的证明论陈述，并表明它有助于结果的发现和呈现。
作者：Xavier Leroy (INRIA Rocquencourt), Herv''e Grall (INRIA Rennes, LINA)
论文ID：0808.0586
分类：Programming Languages
分类简称：cs.PL
提交时间：2008-08-06