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.

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Keiko Nakata, Tarmo Uustalu
• Keywords: Artificial Intelligence, Functional Semantics, Relational Semantics, Semantics, TPHOL 2009