Weakly Final Coalgebras in Dependent Type Theory

Anton Setzer


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.
Tuesday 29th June 2004, 14:00
Robert Recorde Room
Department of Computer Science