TY - GEN
T1 - Trace-based coinductive operational semantics for while
AU - Nakata, Keiko
AU - Uustalu, Tarmo
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350325123&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03359-9_26
DO - 10.1007/978-3-642-03359-9_26
M3 - Conference contribution
AN - SCOPUS:70350325123
SN - 364203358X
SN - 9783642033582
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 375
EP - 390
BT - Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings
T2 - 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009
Y2 - 17 August 2009 through 20 August 2009
ER -