## Trace-based coinductive operational semantics for While:
big-step and small-step styles

Institute of Cybernetics

Thursday, 23 April 2009, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: I will present big-step and small-step operational
semantics, coinductively defined, for the While language. The big-step
semantics defines the behavior of a program in terms of the behavior
of its parts; the small-step semantics defines the behavior of a
program in terms of one-step reduction relations, which relate a
program-state pair to the next program-state pair or the terminal
state. Being defined coinductively, the two semantics describe both
terminating and non-terminating program executions. Moreover the two
semantics are proved equivalent. My talk shall start by considering
inductive and coinductive lists and explaining their uses in Coq, a
type-theory based proof assistant; the operational semantics use
coinductive lists to keep track of all the intermediate states of
possibly non-terminating executions.

(Joint work with Tarmo Uustalu.)

Tarmo Uustalu

Last update 20.4.2009