eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2005-05-20
4381
1
8
10.4230/DagSemProc.04381.1
article
04381 Abstracts Collection – Dependently Typed Programming
Altenkirch, Thorsten
Hofmann, Martin
Hughes, John
From 12.09.04 to 17.09.04, the Dagstuhl Seminar 04381
``Dependently Typed Programming'' was held
in the International Conference and Research Center (IBFI),
Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol04381/DagSemProc.04381.1/DagSemProc.04381.1.pdf
dependently typed programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2005-05-20
4381
1
30
10.4230/DagSemProc.04381.2
article
Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)
Setzer, Anton
Hancock, Peter
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 command-response 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 non-monadic. 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.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol04381/DagSemProc.04381.2/DagSemProc.04381.2.pdf
Dependently types programming
interactive programs
coalgebras
weakly final coalgebras
coiteration
corecursion
monad