(Swansea)

We reconsider the formulation of interactive programs in dependent type theory and note that interactive programs correspond to a special case of weakly final coalgebras. We then introduce rules for weakly final coalgebras of strictly positive functors in dependent type theory. We arrive at the notion of coiteration and investigate its relationship to guarded induction. Finally we explore the relationship between state dependent coalgebras and bisimulation.Robert Recorde Room

Department of Computer Science