User loginNavigation |
Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory
Quite a mouthful, I wonder if it would attract more people if it were titled "Interactive programming in Epigram" :-)
Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory In this article we are going to explore one approach to the representation of interactive programs in dependent type theory. The approach we take centres on the concept of "monadic IO" used in functional programming. We will see that in dependent type theory, besides non-dependent interactive programs in which the interface between the user and the real world is fixed, as in ordinary functional programming, there is a natural notion of state-dependent interactive programs, in which the interface changes over time. |
Browse archives
Active forum topics
|
Recent comments
11 weeks 1 day ago
15 weeks 2 days ago
17 weeks 3 hours ago
17 weeks 3 hours ago
19 weeks 4 days ago
24 weeks 2 days ago
24 weeks 2 days ago
24 weeks 5 days ago
24 weeks 5 days ago
27 weeks 4 days ago