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.)