## Resumptions, weak bisimilarity and big-step semantics for
interactive input-output:

an exercise in mixed induction-coinduction

Institute of Cybernetics

Thursday, 13 May 2010, 16:00 (note the unusual time!)

Cybernetica Bldg (Akadeemia tee 21), room B401

Slides from the talk [pdf]

**Abstract**: We study the question of how to design big-step
semantic descriptions for languages where programs need not terminate,
but some actions they perform (like interactive I/O) are
observable. This is relevant, e.g., in compiler correctness and
program verification. We look at the problem through the glasses of
constructive type theory.

We define several big-step semantics of a suitable extension of
While, based on resumptions and termination-sensitive weak
bisimilarity.

After first considering a basic semantics of statements in terms of
resumptions with explicit internal actions (delays), we introduce a
a variation where resumptions are delay-free: essentially, finite
sequences of delays are removed on the fly from those resumptions that
are responsive (keep performing observable actions every now and then).
We also look at a semantics where delay-free resumptions are
augmented with a silent divergence option. This variation hinges
on ahead-of-time commitments between convergence and divergence.
Classically, it is equivalent to the basic one.

The whole enterprise is an exercise in mixing induction and
coinduction, which is interesting both mathematically and from the
point-of-view of implementing it in a proof assistant. We have fully
formalized our development in Coq.

Joint work with Keiko Nakata.

Tarmo Uustalu

Last update 19 May 2010