Abstract
We reconsider the representation of interactive programs in dependent type theory that the authors proposed in earlier papers. Whereas in previous versions the type of interactive programs was introduced in an ad hoc way, it is here defined as a weakly final coalgebra for a general form of polynomial functor. The are two versions: in the first the interface with the real world is fixed, while in the second the potential interactions can depend on the history of previous interactions. The second version may be appropriate for working with specifications of interactive programs. We focus on commandresponse interfaces, and consider both client and server programs, that run on opposite sides such an interface. We give formation/introduction/elimination/equality rules for these coalgebras. These are explored in two dimensions: coiterative versus corecursive, and monadic versus nonmonadic. We also comment upon the relationship of the corresponding rules with guarded induction. It turns out that the introduction rules are nothing but a slightly restricted form of guarded induction. However, the form in which we write guarded induction is not recursive equations (which would break normalisation  we show that type checking becomes undecidable), but instead involves an elimination operator in a crucial way.
BibTeX  Entry
@InProceedings{setzer_et_al:DSP:2005:176,
author = {Anton Setzer and Peter Hancock},
title = {Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)},
booktitle = {Dependently Typed Programming},
year = {2005},
editor = {Thorsten Altenkirch and Martin Hofmann and John Hughes},
number = {04381},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2005/176},
annote = {Keywords: Dependently types programming , interactive programs , coalgebras , weakly final coalgebras , coiteration , corecursion , monad}
}
Keywords: 

Dependently types programming , interactive programs , coalgebras , weakly final coalgebras , coiteration , corecursion , monad 
Seminar: 

04381  Dependently Typed Programming 
Issue Date: 

2005 
Date of publication: 

20.05.2005 