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
12 weeks 1 day ago
12 weeks 1 day ago
12 weeks 1 day ago
34 weeks 2 days ago
38 weeks 4 days ago
40 weeks 2 days ago
40 weeks 2 days ago
42 weeks 6 days ago
47 weeks 4 days ago
47 weeks 4 days ago