1: \begin{abstract}

2:   We look at the operational semantics of languages with interactive

3:   I/O through the glasses of constructive type theory. Following on

4:   from our earlier work on coinductive trace-based semantics for While

5:   \cite{NU:trabco}, we define several big-step semantics for While

6:   with interactive I/O, based on resumptions and termination-sensitive

7:   weak bisimilarity. These require nesting inductive definitions in

8:   coinductive definitions, which is interesting both mathematically

9:   and from the point-of-view of implementation in a proof assistant.

10:   

11:   After first defining a basic semantics of statements in terms of

12:   resumptions with explicit internal actions (delays), we introduce a

13:   semantics in terms of delay-free resumptions that essentially

14:   removes finite sequences of delays on the fly from those resumptions

15:   that are responsive. Finally, we also look at a semantics in terms

16:   of delay-free resumptions supplemented with a silent divergence

17:   option.  This semantics hinges on decisions between convergence and

18:   divergence and is only equivalent to the basic one

19:   classically.

20: %

21:   We have fully formalized our development in Coq.

22: \end{abstract}

23: