Sciweavers

Share
TPHOL
2009
IEEE

Trace-Based Coinductive Operational Semantics for While

10 years 4 months ago
Trace-Based Coinductive Operational Semantics for While
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.
Keiko Nakata, Tarmo Uustalu
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Keiko Nakata, Tarmo Uustalu
Comments (0)
books