Coinductive big-step operational semantics
Coinductive big-step operational semantics
复制标题
DOI：
10.1016/j.ic.2007.12.004
复制
发表时间：
2009-02-01
影响因子：
1
通讯作者：
Grall, Herve
中科院分区：
文献类型：
--
作者：
Leroy, Xavier;Grall, Herve
本文以一个按值调用的函数式语言为例，说明了在大步操作语义中共归纳定义和证明的使用，使其能够描述除了终止求值之外的发散求值。我们正式的共归纳大步语义和标准的小步语义之间的连接，证明这两种语义是等价的。然后，我们研究使用共归纳大步语义证明类型的可靠性和证明的语义保存编译器。本文的一个方法上的独创性是，所有的结果都证明了使用Coq证明助手。我们解释了Coq提供的共归纳定义和证明的证明理论介绍，并表明它有利于发现和介绍的结果。(c)2008年爱思唯尔公司All rights reserved.
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results. (c) 2008 Elsevier Inc. All rights reserved.