Trace-Based Coinductive Operational Semantics for While

Trace-Based Coinductive Operational Semantics for While
复制标题

While 的基于跟踪的共导操作语义

DOI：
--
复制
发表时间：
2009
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
通讯作者：
Tarmo Uustalu
Tarmo Uustalu
中科院分区：
--
文献类型：
--
作者：
Keiko Nakata;Tarmo Uustalu

文献摘要

被引文献

相似文献

我们给出了While语言的四种协同归纳操作语义：大步和小步关系语义和大步和小步函数语义。语义使用跟踪(可能是无限的状态序列)来记录程序运行所经历的状态。关系语义将语句-状态对与跟踪相关联，而函数语义返回语句-状态对的跟踪。这四种语义都是等价的。我们在Coq的构造性环境下形式化了语义及其等价证明。
We present four coinductive operational semantics for the While language accounting for both terminating and non-terminating program runs: big-step and small-step relational semantics and big-step and small-step functional semantics. The semantics employ traces (possibly infinite sequences of states) to record the states that program runs go through. The relational semantics relate statement-state pairs to traces, whereas the functional semantics return traces for statement-state pairs. All four semantics are equivalent. We formalize the semantics and their equivalence proofs in the constructive setting of Coq.