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 semant...
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for W...